// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

div_mod.let_clause_1078

Statement

∀ a b q r q1 r1, div_mod_spec a b q r ⇒ r < b ⇒ a = ((q × b) + r) ⇒ div_mod_spec a b q1 r1 ⇒ r1 < b ⇒ a = ((q1 × b) + r1) ⇒ q ≤ q1 ⇒ q < q1 ⇒ a = (r + (b × q))

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem let_clause_1078 : forall (a:nat.nat), forall (b:nat.nat), forall (q:nat.nat), forall (r:nat.nat), forall (q1:nat.nat), forall (r1:nat.nat), (div_mod_spec a b q r) -> (nat.lt r b) -> (logic.eq (nat.nat) a (nat.plus (nat.times q b) r)) -> (div_mod_spec a b q1 r1) -> (nat.lt r1 b) -> (logic.eq (nat.nat) a (nat.plus (nat.times q1 b) r1)) -> (nat.le q q1) -> (nat.lt q q1) -> logic.eq (nat.nat) a (nat.plus r (nat.times b q)).



Matita-Jumb
Statement

theorem let_clause_1078 : \forall (a:nat). \forall (b:nat). \forall (q:nat). \forall (r:nat). \forall (q1:nat). \forall (r1:nat). ((div_mod_spec) a b q r) -> ((lt) r b) -> ((eq) (nat) a ((plus) ((times) q b) r)) -> ((div_mod_spec) a b q1 r1) -> ((lt) r1 b) -> ((eq) (nat) a ((plus) ((times) q1 b) r1)) -> ((le) q q1) -> ((lt) q q1) -> (eq) (nat) a ((plus) r ((times) b q)).



Lean-jumb
Statement

theorem let_clause_1078 : forall (a:nat.nat) , forall (b:nat.nat) , forall (q:nat.nat) , forall (r:nat.nat) , forall (q1:nat.nat) , forall (r1:nat.nat) , ((((((div_mod.div_mod_spec) ) (a)) (b)) (q)) (r)) -> ((((nat.lt_) ) (r)) (b)) -> ((((logic.eq_) (nat.nat)) (a)) ((((nat.plus) ) ((((nat.times) ) (q)) (b))) (r))) -> ((((((div_mod.div_mod_spec) ) (a)) (b)) (q1)) (r1)) -> ((((nat.lt_) ) (r1)) (b)) -> ((((logic.eq_) (nat.nat)) (a)) ((((nat.plus) ) ((((nat.times) ) (q1)) (b))) (r1))) -> ((((nat.le_) ) (q)) (q1)) -> ((((nat.lt_) ) (q)) (q1)) -> (((logic.eq_) (nat.nat)) (a)) ((((nat.plus) ) (r)) ((((nat.times) ) (b)) (q))).



PVS-jumb

Statement

let_clause_1078 : LEMMA (FORALL(a:nat_sttfa_th.sttfa_nat):(FORALL(b:nat_sttfa_th.sttfa_nat):(FORALL(q:nat_sttfa_th.sttfa_nat):(FORALL(r:nat_sttfa_th.sttfa_nat):(FORALL(q1:nat_sttfa_th.sttfa_nat):(FORALL(r1:nat_sttfa_th.sttfa_nat):(div_mod_sttfa.div_mod_spec(a)(b)(q)(r) => (nat_sttfa_th.lt(r)(b) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](a)(nat_sttfa_th.plus(nat_sttfa_th.times(q)(b))(r)) => (div_mod_sttfa.div_mod_spec(a)(b)(q1)(r1) => (nat_sttfa_th.lt(r1)(b) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](a)(nat_sttfa_th.plus(nat_sttfa_th.times(q1)(b))(r1)) => (nat_sttfa_th.le(q)(q1) => (nat_sttfa_th.lt(q)(q1) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](a)(nat_sttfa_th.plus(r)(nat_sttfa_th.times(b)(q)))))))))))))))))



OpenTheory

Printing for OpenTheory is not working at the moment.