commit by user andrea

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index 9432984443838055615e9d56aa3fdc371a709d5c..ec11cf2ec002457254c6a2094ce13bbd0a1a5155 100644 (file)
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -1,8 +1,53 @@
 (* new script *)
 
-include "While/syntax.ma".  
+include "While/syntax.ma". 
+include "arithmetics/div_and_mod.ma. 
 
 
 (* state *)
 
-definition state ≝ \
\ No newline at end of file
+definition state ≝ \ 5a href="cic:/matita/While/syntax/Var.ind(1,0,0)"\ 6Var\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+
+(* Semantics of Arithmetic expressions *)
+
+\ 5pre class="smallmargin" style="display: inline;"\ 6let rec eval_Aexp a s ≝
+  match a with 
+  | Const n => n
+  | Aid v => s v
+  | Add a b => a+b
+  | Sub a b => a-b
+  | Mul a b => a*b
+  | Div a b => div a b
+  | Mod a b => mod a b
+ .
+
+interpretation "Aexp plus" 'plus x y = (Add x y).
+interpretation "Aexp minus" 'plus x y = (Sub x y).
+interpretation "Aexp times" 'times x y = (Mul x y).
+
+(* Boolean expressions *)
+inductive Bexp : Type[0] ≝
+  | BFalse : Bexp
+  | BTtrue : Bexp
+  | BNot : Bexp → Bexp
+  | BAnd : Bexp → Bexp → Bexp
+  | BOr : Bexp → Bexp → Bexp
+  | Eq : \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Bexp
+  | LE : \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Bexp
+.
+
+interpretation "Bexp not" 'not x = (BNot x).
+interpretation "Bexp and" 'and x y = (BAnd x y).
+interpretation "Bexp or" 'or x y = (BOr x y).
+interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y).
+
+(* Commands *)
+inductive Cmd : Type[0] ≝
+  | Skip : Cmd
+  | Assign : Var → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Cmd
+  | Seq : Cmd → Cmd → Cmd
+  | If : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd → Cmd
+  | While : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd
+.
+
+\ 5/pre\ 6 
\ No newline at end of file

diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma
index b55d89d438b7f238f013830fed30b36d9765bb4f..95c93c7e4984816df4948c930c68aa84152dc5e6 100644 (file)
--- a/weblib/While/syntax.ma
+++ b/weblib/While/syntax.ma
@@ -7,7 +7,7 @@ include "arithmetics/nat.ma".
 
 (* Variables *)
 
-inductive Var : Type[0] ≝
+ inductive Var : Type[0] ≝
   Id : nat → Var.
  
 (* Arithmetic expressions *)

diff --git a/weblib/arithmetics/div_and_mod.ma b/weblib/arithmetics/div_and_mod.ma
index 4044695d221c775f833f90f212f09e7397d86942..d7c5b4e06922588051711969402796c4e90f1d83 100644 (file)
--- a/weblib/arithmetics/div_and_mod.ma
+++ b/weblib/arithmetics/div_and_mod.ma
@@ -11,158 +11,151 @@
 
 include "arithmetics/nat.ma".
 
-let rec mod_aux p m n: nat ≝
+\ 5img class="anchor" src="icons/tick.png" id="mod_aux"\ 6let rec mod_aux p m n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 ≝
 match p with
   [ O ⇒ m
-  | S q ⇒ match (leb m n) with
+  | S q ⇒ match (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n) with
     [ true ⇒ m
-    | false ⇒ mod_aux q (m-(S n)) n]].
+    | false ⇒ mod_aux q (m\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) n]].
 
-definition mod : nat → nat → nat ≝
+\ 5img class="anchor" src="icons/tick.png" id="mod"\ 6definition mod : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 ≝
 λn,m. match m with 
   [ O ⇒ n
-  | S p ⇒ mod_aux n n p]. 
+  | S p ⇒ \ 5a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"\ 6mod_aux\ 5/a\ 6 n n p]. 
 
 interpretation "natural remainder" 'module x y = (mod x y).
 
-let rec div_aux p m n : nat ≝
+\ 5img class="anchor" src="icons/tick.png" id="div_aux"\ 6let rec div_aux p m n : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 ≝
 match p with
-  [ O ⇒ O
-  | S q ⇒ match (leb m n) with
-    [ true ⇒ O
-    | false ⇒ S (div_aux q (m-(S n)) n)]].
+  [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
+  | S q ⇒ match (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n) with
+    [ true ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
+    | false ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (div_aux q (m\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) n)]].
 
-definition div : nat → nat → nat ≝
+\ 5img class="anchor" src="icons/tick.png" id="div"\ 6definition div : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 ≝
 λn,m.match m with 
-  [ O ⇒ S n
-  | S p ⇒ div_aux n n p]. 
+  [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n
+  | S p ⇒ \ 5a href="cic:/matita/arithmetics/div_and_mod/div_aux.fix(0,0,2)"\ 6div_aux\ 5/a\ 6 n n p]. 
 
 interpretation "natural divide" 'divide x y = (div x y).
 
-theorem le_mod_aux_m_m: 
-∀p,n,m. n ≤ p → mod_aux p n m ≤ m.
+\ 5img class="anchor" src="icons/tick.png" id="le_mod_aux_m_m"\ 6theorem le_mod_aux_m_m: 
+∀p,n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p → \ 5a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"\ 6mod_aux\ 5/a\ 6 p n m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
 #p (elim p)
-[ normalize #n #m #lenO @(le_n_O_elim …lenO) //
+[ normalize #n #m #lenO @(\ 5a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"\ 6le_n_O_elim\ 5/a\ 6 …lenO) //
 | #q #Hind #n #m #len normalize 
-    @(leb_elim n m) normalize //
-    #notlenm @Hind @le_plus_to_minus
-    @(transitive_le … len) /2/
+    @(\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 n m) normalize //
+    #notlenm @Hind @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"\ 6le_plus_to_minus\ 5/a\ 6
+    @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … len) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 qed.
 
-theorem lt_mod_m_m: ∀n,m. O < m → n \mod m  < m.
+\ 5img class="anchor" src="icons/tick.png" id="lt_mod_m_m"\ 6theorem lt_mod_m_m: ∀n,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m  \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m.
 #n #m (cases m) 
-  [#abs @False_ind /2/
-  |#p #_ normalize @le_S_S /2/ 
+  [#abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |#p #_ normalize @\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/div_and_mod/le_mod_aux_m_m.def(11)"\ 6le_mod_aux_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ 
   ]
 qed.
 
-theorem div_aux_mod_aux: ∀p,n,m:nat. 
-n=(div_aux p n m)*(S m) + (mod_aux p n m).
+\ 5img class="anchor" src="icons/tick.png" id="div_aux_mod_aux"\ 6theorem div_aux_mod_aux: ∀p,n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. 
+n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_aux.fix(0,0,2)"\ 6div_aux\ 5/a\ 6 p n m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"\ 6mod_aux\ 5/a\ 6 p n m).
 #p (elim p)
   [#n #m normalize //
   |#q #Hind #n #m normalize
-     @(leb_elim n m) #lenm normalize //
-     >associative_plus <(Hind (n-(S m)) m)
-     applyS plus_minus_m_m (* bello *) /2/
+     @(\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 n m) #lenm normalize //
+     >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <(Hind (n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) m)
+     applyS \ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 (* bello *) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
-theorem div_mod: ∀n,m:nat. n=(n / m)*m+(n \mod m).
+\ 5img class="anchor" src="icons/tick.png" id="div_mod"\ 6theorem div_mod: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m).
 #n #m (cases m) normalize //
 qed.
 
-theorem eq_times_div_minus_mod:
-∀a,b:nat. (a / b) * b = a - (a \mod b).
-#a #b (applyS minus_plus_m_m) qed.
+\ 5img class="anchor" src="icons/tick.png" id="eq_times_div_minus_mod"\ 6theorem eq_times_div_minus_mod:
+∀a,b:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. (a \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 b) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 (a \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 b).
+#a #b (applyS \ 5a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"\ 6minus_plus_m_m\ 5/a\ 6) qed.
 
-inductive div_mod_spec (n,m,q,r:nat) : Prop ≝
-div_mod_spec_intro: r < m → n=q*m+r → div_mod_spec n m q r.
+\ 5img class="anchor" src="icons/tick.png" id="div_mod_spec"\ 6inductive div_mod_spec (n,m,q,r:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) : Prop ≝
+div_mod_spec_intro: r \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6r → div_mod_spec n m q r.
 
-theorem div_mod_spec_to_not_eq_O: 
-  ∀n,m,q,r.div_mod_spec n m q r → m ≠ O.
-#n #m #q #r * /2/ 
+\ 5img class="anchor" src="icons/tick.png" id="div_mod_spec_to_not_eq_O"\ 6theorem div_mod_spec_to_not_eq_O: 
+  ∀n,m,q,r.\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 n m q r → m \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+#n #m #q #r * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ 
 qed.
 
-theorem div_mod_spec_div_mod: 
-  ∀n,m. O < m → div_mod_spec n m (n / m) (n \mod m).
-#n #m #posm % /2/ qed.
+\ 5img class="anchor" src="icons/tick.png" id="div_mod_spec_div_mod"\ 6theorem div_mod_spec_div_mod: 
+  ∀n,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 n m (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m) (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m).
+#n #m #posm % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
 
-theorem div_mod_spec_to_eq :∀ a,b,q,r,q1,r1.
-div_mod_spec a b q r → div_mod_spec a b q1 r1 → q = q1.
+\ 5img class="anchor" src="icons/tick.png" id="div_mod_spec_to_eq"\ 6theorem div_mod_spec_to_eq :∀ a,b,q,r,q1,r1.
+\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 a b q r → \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 a b q1 r1 → q \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 q1.
 #a #b #q #r #q1 #r1 * #ltrb #spec *  #ltr1b #spec1
-@(leb_elim q q1) #leqq1
-  [(elim (le_to_or_lt_eq … leqq1)) //
-     #ltqq1 @False_ind @(absurd ?? (not_le_Sn_n a))
-     @(lt_to_le_to_lt ? ((S q)*b) ?)
-      [>spec (applyS (monotonic_lt_plus_r … ltrb))
-      |@(transitive_le ? (q1*b)) /2/
+@(\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 q q1) #leqq1
+  [(elim (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … leqq1)) //
+     #ltqq1 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ?? (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_n.def(6)"\ 6not_le_Sn_n\ 5/a\ 6 a))
+     @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 q)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b) ?)
+      [>spec (applyS (\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_r.def(9)"\ 6monotonic_lt_plus_r\ 5/a\ 6 … ltrb))
+      |@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (q1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
       ]
   (* this case is symmetric *)
-  |@False_ind @(absurd ?? (not_le_Sn_n a))
-     @(lt_to_le_to_lt ? ((S q1)*b) ?)
-      [>spec1 (applyS (monotonic_lt_plus_r … ltr1b))
-      |cut (q1 < q) [/2/] #ltq1q @(transitive_le ? (q*b)) /2/
+  |@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ?? (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_n.def(6)"\ 6not_le_Sn_n\ 5/a\ 6 a))
+     @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 q1)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b) ?)
+      [>spec1 (applyS (\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_r.def(9)"\ 6monotonic_lt_plus_r\ 5/a\ 6 … ltr1b))
+      |cut (q1 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] #ltq1q @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
       ]
   ]
 qed.
 
-theorem div_mod_spec_to_eq2: ∀a,b,q,r,q1,r1.
-  div_mod_spec a b q r → div_mod_spec a b q1 r1 → r = r1.
+\ 5img class="anchor" src="icons/tick.png" id="div_mod_spec_to_eq2"\ 6theorem div_mod_spec_to_eq2: ∀a,b,q,r,q1,r1.
+  \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 a b q r → \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 a b q1 r1 → r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 r1.
 #a #b #q #r #q1 #r1 #spec #spec1
-cut (q=q1) [@(div_mod_spec_to_eq … spec spec1)] 
+cut (q\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6q1) [@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 … spec spec1)] 
 #eqq (elim spec) #_ #eqa (elim spec1) #_ #eqa1 
-@(injective_plus_r (q*b)) //
+@(\ 5a href="cic:/matita/arithmetics/nat/injective_plus_r.def(5)"\ 6injective_plus_r\ 5/a\ 6 (q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b)) //
 qed.
 
-(* boh
-theorem div_mod_spec_times : ∀ n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
-intros.constructor 1.
-unfold lt.apply le_S_S.apply le_O_n. demodulate. reflexivity.
-(*rewrite < plus_n_O.rewrite < sym_times.reflexivity.*)
-qed. *)
-
-lemma div_plus_times: ∀m,q,r:nat. r < m → (q*m+r)/ m = q.
+\ 5img class="anchor" src="icons/tick.png" id="div_plus_times"\ 6lemma div_plus_times: ∀m,q,r:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. r \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → (q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6r)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 q.
 #m #q #r #ltrm
-@(div_mod_spec_to_eq … (div_mod_spec_div_mod ???)) /2/
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 ???)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"\ 6ltn_to_ltO\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
-lemma mod_plus_times: ∀m,q,r:nat. r < m → (q*m+r) \mod m = r. 
+\ 5img class="anchor" src="icons/tick.png" id="mod_plus_times"\ 6lemma mod_plus_times: ∀m,q,r:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. r \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → (q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6r) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 r. 
 #m #q #r #ltrm
-@(div_mod_spec_to_eq2 … (div_mod_spec_div_mod ???)) /2/
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 ???)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"\ 6ltn_to_ltO\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
 (* some properties of div and mod *)
-theorem div_times: ∀a,b:nat. O < b → a*b/b = a.
+\ 5img class="anchor" src="icons/tick.png" id="div_times"\ 6theorem div_times: ∀a,b:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b → a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
 #a #b #posb 
-@(div_mod_spec_to_eq (a*b) b … O (div_mod_spec_div_mod …))
-// @div_mod_spec_intro // qed.
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 (a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b) b … \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
+// @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6 // qed.
 
-theorem div_n_n: ∀n:nat. O < n → n / n = 1.
-/2/ qed.
+\ 5img class="anchor" src="icons/tick.png" id="div_n_n"\ 6theorem div_n_n: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6.
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
 
-theorem eq_div_O: ∀n,m. n < m → n / m = O.
+\ 5img class="anchor" src="icons/tick.png" id="eq_div_O"\ 6theorem eq_div_O: ∀n,m. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
 #n #m #ltnm 
-@(div_mod_spec_to_eq n m (n/m) … n (div_mod_spec_div_mod …))
-/2/ qed. 
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 n m (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) … n (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"\ 6ltn_to_ltO\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
 
-theorem mod_n_n: ∀n:nat. O < n → n \mod n = O.
+\ 5img class="anchor" src="icons/tick.png" id="mod_n_n"\ 6theorem mod_n_n: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
 #n #posn 
-@(div_mod_spec_to_eq2 n n … 1 0 (div_mod_spec_div_mod …))
-/2/ qed. 
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n n … \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
 
-theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m → 
-((S n) \mod m) = S (n \mod m).
+\ 5img class="anchor" src="icons/tick.png" id="mod_S"\ 6theorem mod_S: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m) \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → 
+((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m).
 #n #m #posm #H 
-@(div_mod_spec_to_eq2 (S n) m … (n / m) ? (div_mod_spec_div_mod …))
-// @div_mod_spec_intro// (applyS eq_f) //
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) m … (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m) ? (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
+// @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6// (applyS \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6) //
 qed.
 
-theorem mod_O_n: ∀n:nat.O \mod n = O.
-/2/ qed.
+\ 5img class="anchor" src="icons/tick.png" id="mod_O_n"\ 6theorem mod_O_n: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"\ 6plus_minus\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
 
-theorem lt_to_eq_mod: ∀n,m:nat. n < m → n \mod m = n.
+\ 5img class="anchor" src="icons/tick.png" id="lt_to_eq_mod"\ 6theorem lt_to_eq_mod: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
 #n #m #ltnm 
-@(div_mod_spec_to_eq2 n m (n/m) … O n (div_mod_spec_div_mod …))
-/2/ qed. 
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n m (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) … \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 n (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"\ 6ltn_to_ltO\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
 
 (*
 theorem mod_1: ∀n:nat. mod n 1 = O.
@@ -172,26 +165,26 @@ theorem mod_1: ∀n:nat. mod n 1 = O.
 theorem div_1: ∀n:nat. div n 1 = n.
 #n @sym_eq napplyS (div_mod n 1) qed. *)
 
-theorem or_div_mod: ∀n,q. O < q →
-  ((S (n \mod q)=q) ∧ S n = (S (div n q)) * q ∨
-  ((S (n \mod q)<q) ∧ S n = (div n q) * q + S (n\mod q))).
+\ 5img class="anchor" src="icons/tick.png" id="or_div_mod"\ 6theorem or_div_mod: ∀n,q. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q →
+  ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6q) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 n q)) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 q \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6
+  ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6q) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 n q) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 q \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q))).
 #n #q #posq 
-(elim (le_to_or_lt_eq ?? (lt_mod_m_m n q posq))) #H
-  [%2 % // (applyS eq_f) //
-  |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)) @eq_f//
+(elim (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 ?? (\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 n q posq))) #H
+  [%2 % // (applyS \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6) //
+  |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)); @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6//
   ]
 qed.
 
 (* injectivity *)
-theorem injective_times_r: 
-  ∀n:nat. O < n → injective nat nat (λm:nat.n*m).
+\ 5img class="anchor" src="icons/tick.png" id="injective_times_r"\ 6theorem injective_times_r: 
+  ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 (λm:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m).
 #n #posn #a #b #eqn 
-<(div_times a n posn) <(div_times b n posn) // 
+<(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6 a n posn) <(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6 b n posn) // 
 qed.
 
-theorem injective_times_l: 
-    ∀n:nat. O < n → injective nat nat (λm:nat.m*n).
-/2/ qed.
+\ 5img class="anchor" src="icons/tick.png" id="injective_times_l"\ 6theorem injective_times_l: 
+    ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 (λm:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n).
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/injective_times_r.def(15)"\ 6injective_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
 
 (* n_divides computes the pair (div,mod) 
 (* p is just an upper bound, acc is an accumulator *)
@@ -208,64 +201,64 @@ definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. *)
 
 (* inequalities *)
 
-theorem lt_div_S: ∀n,m. O < m → n < S(n / m)*m.
-#n #m #posm (change with (n < m +(n/m)*m))
->(div_mod n m) in ⊢ (? % ?) >commutative_plus 
-@monotonic_lt_plus_l @lt_mod_m_m // 
+\ 5img class="anchor" src="icons/tick.png" id="lt_div_S"\ 6theorem lt_div_S: ∀n,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m.
+#n #m #posm (change with (n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m))
+>(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 n m) in ⊢ (? % ?); >\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 
+@\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"\ 6monotonic_lt_plus_l\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 // 
 qed.
 
-theorem le_div: ∀n,m. O < n → m/n ≤ m.
+\ 5img class="anchor" src="icons/tick.png" id="le_div"\ 6theorem le_div: ∀n,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
 #n #m #posn
->(div_mod m n) in ⊢ (? ? %) @(transitive_le ? (m/n*n)) /2/
+>(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 m n) in ⊢ (? ? %); @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
-theorem le_plus_mod: ∀m,n,q. O < q →
-(m+n) \mod q ≤ m \mod q + n \mod q .
+\ 5img class="anchor" src="icons/tick.png" id="le_plus_mod"\ 6theorem le_plus_mod: ∀m,n,q. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q →
+(m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q .
 #m #n #q #posq
-(elim (decidable_le q (m \mod q + n \mod q))) #Hle
-  [@(transitive_le … Hle) @le_S_S_to_le @le_S /2/
-  |cut ((m+n)\mod q = m\mod q+n\mod q) //
-     @(div_mod_spec_to_eq2 … (m/q + n/q) ? (div_mod_spec_div_mod … posq)).
-     @div_mod_spec_intro
-      [@not_le_to_lt //
-      |>(div_mod n q) in ⊢ (? ? (? ? %) ?)
-       (applyS (eq_f … (λx.plus x (n \mod q))))
-       >(div_mod m q) in ⊢ (? ? (? % ?) ?)
-       (applyS (eq_f … (λx.plus x (m \mod q)))) //
+(elim (\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a\ 6 q (m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q))) #Hle
+  [@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … Hle) @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |cut ((m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n)\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q) //
+     @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 … (m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q) ? (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 … posq)).
+     @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6
+      [@\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 //
+      |>(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 n q) in ⊢ (? ? (? ? %) ?);
+       (applyS (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 … (λx.\ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6 x (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q))))
+       >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 m q) in ⊢ (? ? (? % ?) ?);       
+       (applyS (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 … (λx.\ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6 x (m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)))) //
       ]
   ]
 qed.
 
-theorem le_plus_div: ∀m,n,q. O < q →
-  m/q + n/q \le (m+n)/q.
-#m #n #q #posq @(le_times_to_le … posq)
-@(le_plus_to_le_r ((m+n) \mod q))
+\ 5img class="anchor" src="icons/tick.png" id="le_plus_div"\ 6theorem le_plus_div: ∀m,n,q. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q →
+  m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\le\ 5/a\ 6 (m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q.
+#m #n #q #posq @(\ 5a href="cic:/matita/arithmetics/nat/le_times_to_le.def(9)"\ 6le_times_to_le\ 5/a\ 6 … posq)
+@(\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"\ 6le_plus_to_le_r\ 5/a\ 6 ((m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q))
 (* bruttino *)
->commutative_times in ⊢ (? ? %) <div_mod
->(div_mod m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %))
->commutative_plus in ⊢ (? ? (? % ?)) >associative_plus in ⊢ (? ? %)
-<associative_plus in ⊢ (? ? (? ? %)) (applyS monotonic_le_plus_l) /2/
+>\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 in ⊢ (? ? %); <\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6
+>(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 m q) in ⊢ (? ? (? % ?)); >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 n q) in ⊢ (? ? (? ? %));
+>\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 in ⊢ (? ? (? % ?)); >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 in ⊢ (? ? %);
+<\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 in ⊢ (? ? (? ? %)); (applyS \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"\ 6monotonic_le_plus_l\ 5/a\ 6) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/le_plus_mod.def(14)"\ 6le_plus_mod\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
-theorem le_times_to_le_div: ∀a,b,c:nat. 
-  O < b → b*c ≤ a → c ≤ a/b.
+\ 5img class="anchor" src="icons/tick.png" id="le_times_to_le_div"\ 6theorem le_times_to_le_div: ∀a,b,c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. 
+  \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b → b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 a → c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b.
 #a #b #c #posb #Hle
-@le_S_S_to_le @(lt_times_n_to_lt_l b) @(le_to_lt_to_lt ? a)/2/
+@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"\ 6lt_times_n_to_lt_l\ 5/a\ 6 b) @(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"\ 6le_to_lt_to_lt\ 5/a\ 6 ? a)/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_div_S.def(13)"\ 6lt_div_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
-theorem le_times_to_le_div2: ∀m,n,q. O < q → 
-  n ≤ m*q → n/q ≤ m.
+\ 5img class="anchor" src="icons/tick.png" id="le_times_to_le_div2"\ 6theorem le_times_to_le_div2: ∀m,n,q. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q → 
+  n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q → n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
 #m #n #q #posq #Hle
-@(le_times_to_le q ? ? posq) @(le_plus_to_le (n \mod q)) /2/
+@(\ 5a href="cic:/matita/arithmetics/nat/le_times_to_le.def(9)"\ 6le_times_to_le\ 5/a\ 6 q ? ? posq) @(\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"\ 6le_plus_to_le\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_a.def(8)"\ 6le_plus_a\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
 (* da spostare 
 theorem lt_m_nm: ∀n,m. O < m → 1 < n → m < n*m.
 /2/ qed. *)
    
-theorem lt_times_to_lt_div: ∀m,n,q. n < m*q → n/q < m.
+\ 5img class="anchor" src="icons/tick.png" id="lt_times_to_lt_div"\ 6theorem lt_times_to_lt_div: ∀m,n,q. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q → n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m.
 #m #n #q #Hlt
-@(lt_times_n_to_lt_l q …) @(lt_plus_to_lt_l (n \mod q)) /2/
+@(\ 5a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"\ 6lt_times_n_to_lt_l\ 5/a\ 6 q …) @(\ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"\ 6lt_plus_to_lt_l\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
 (*
@@ -282,24 +275,24 @@ theorem le_div_plus_S: ∀m,n,q. O < q →
 //
 qed. *)
 
-theorem le_div_S_S_div: ∀n,m. O < m → (S n)/m ≤ S (n /m).
-#n #m #posm @le_times_to_le_div2 /2/
+\ 5img class="anchor" src="icons/tick.png" id="le_div_S_S_div"\ 6theorem le_div_S_S_div: ∀n,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m).
+#n #m #posm @\ 5a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div2.def(10)"\ 6le_times_to_le_div2\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_div_S.def(13)"\ 6lt_div_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
-theorem le_times_div_div_times: ∀a,n,m.O < m → 
-a*(n/m) ≤ a*n/m. 
-#a #n #m #posm @le_times_to_le_div /2/
+\ 5img class="anchor" src="icons/tick.png" id="le_times_div_div_times"\ 6theorem le_times_div_div_times: ∀a,n,m.\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → 
+a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m. 
+#a #n #m #posm @\ 5a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div.def(14)"\ 6le_times_to_le_div\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 qed.
 
-theorem monotonic_div: ∀n.O < n →
-  monotonic nat le (λm.div m n).
-#n #posn #a #b #leab @le_times_to_le_div/2/
+\ 5img class="anchor" src="icons/tick.png" id="monotonic_div"\ 6theorem monotonic_div: ∀n.\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n →
+  \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"\ 6le\ 5/a\ 6 (λm.\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 m n).
+#n #posn #a #b #leab @\ 5a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div.def(14)"\ 6le_times_to_le_div\ 5/a\ 6/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
-theorem pos_div: ∀n,m:nat. O < m → O < n → n \mod m = O → 
-  O < n / m.
+\ 5img class="anchor" src="icons/tick.png" id="pos_div"\ 6theorem pos_div: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 → 
+  \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m.
 #n #m #posm #posn #mod0
-@(lt_times_n_to_lt_l m)// (* MITICO *)
+@(\ 5a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"\ 6lt_times_n_to_lt_l\ 5/a\ 6 m)// (* MITICO *)
 qed.
 
 (*
@@ -308,135 +301,56 @@ theorem lt_div_n_m_n: ∀n,m:nat. 1 < m → O < n → n / m < n.
 @(leb_elim 1 (n / m))/2/ (* MITICO *)
 qed. *)
 
-theorem eq_div_div_div_times: ∀n,m,q. O < n → O < m →
- q/n/m = q/(n*m).
+\ 5img class="anchor" src="icons/tick.png" id="eq_div_div_div_times"\ 6theorem eq_div_div_div_times: ∀n,m,q. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m →
+ q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6(n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m).
 #n #m #q #posn #posm
-@(div_mod_spec_to_eq … (q\mod n+n*(q/n\mod m)) … (div_mod_spec_div_mod …)) /2/
-@div_mod_spec_intro // @(lt_to_le_to_lt ? (n*(S (q/n\mod m))))
-  [(applyS monotonic_lt_plus_l) /2/
-  |@monotonic_le_times_r/2/
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 … (q\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)) … (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_times.def(13)"\ 6lt_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6 // @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m))))
+  [(applyS \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"\ 6monotonic_lt_plus_l\ 5/a\ 6) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |@\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
   ]
 qed.
 
-theorem eq_div_div_div_div: ∀n,m,q. O < n → O < m →
-q/n/m = q/m/n.
+\ 5img class="anchor" src="icons/tick.png" id="eq_div_div_div_div"\ 6theorem eq_div_div_div_div: ∀n,m,q. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m →
+q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n.
 #n #m #q #posn #posm
-@(trans_eq ? ? (q/(n*m)))
-  [/2/
-  |@sym_eq (applyS eq_div_div_div_times) //
+@(\ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6 ? ? (q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6(n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m)))
+  [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"\ 6eq_div_div_div_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 (applyS \ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"\ 6eq_div_div_div_times\ 5/a\ 6) //
   ]
 qed.
 
-(*
-theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)).
-intros.
-rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
-  [rewrite > eq_div_div_div_div
-    [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
-     apply div_mod.
-     apply lt_O_S
-    |apply lt_O_S
-    |assumption
-    ]
-  |apply lt_O_S
-  ]
-qed. *)
-(* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
-(* The theorem is shown in two different parts: *)
-(*
-theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat.
-O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
-intros.
-split
-[ rewrite < H1.
-  rewrite > sym_times.
-  rewrite > eq_times_div_minus_mod
-  [ apply (le_minus_m a (a \mod b))
-  | assumption
-  ]
-| rewrite < (times_n_Sm b c).
-  rewrite < H1.
-  rewrite > sym_times.
-  rewrite > (div_mod a b) in \vdash (? % ?)
-  [ rewrite > (sym_plus b ((a/b)*b)).
-    apply lt_plus_r.
-    apply lt_mod_m_m.
-    assumption
-  | assumption
-  ]
-]
-qed. *)
-
-theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat.
-O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c.
+\ 5img class="anchor" src="icons/tick.png" id="lt_to_le_times_to_lt_S_to_div"\ 6theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b → (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 a → a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 c)) → a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 c.
 #a #c #b #posb#lea #lta
-@(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …))
-@div_mod_spec_intro [@lt_plus_to_minus // |/2/]
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 … (a\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 … posb …))
+@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6 [@\ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_minus.def(11)"\ 6lt_plus_to_minus\ 5/a\ 6 // |/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"\ 6plus_minus\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
 qed.
 
-theorem div_times_times: ∀a,b,c:nat. O < c → O < b → 
-  (a/b) = (a*c)/(b*c).
+\ 5img class="anchor" src="icons/tick.png" id="div_times_times"\ 6theorem div_times_times: ∀a,b,c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b → 
+  (a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6(b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c).
 #a #b #c #posc #posb
->(commutative_times b) <eq_div_div_div_times //
->div_times //
+>(\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 b) <\ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"\ 6eq_div_div_div_times\ 5/a\ 6 //
+>\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6 //
 qed.
 
-theorem times_mod: ∀a,b,c:nat.
-O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b).
+\ 5img class="anchor" src="icons/tick.png" id="times_mod"\ 6theorem times_mod: ∀a,b,c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b → (a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(a\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 b).
 #a #b #c #posc #posb
-@(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
-  [>(div_times_times … posc) // @div_mod_spec_div_mod /2/
-  |@div_mod_spec_intro
-    [applyS (monotonic_lt_times_r … c posc) /2/
-    |(applyS (eq_f …(λx.x*c))) //
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 (a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) (a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b) ((a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c)) (a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b) (c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(a \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 b)))
+  [>(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times_times.def(15)"\ 6div_times_times\ 5/a\ 6 … posc) // @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_times.def(13)"\ 6lt_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6
+    [applyS (\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"\ 6monotonic_lt_times_r\ 5/a\ 6 … c posc) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+    |(applyS (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 …(λx.x\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c))) //
     ]
   ]
 qed.
 
-theorem le_div_times_m: ∀a,i,m. O < i → O < m →
- (a * (m / i)) / m ≤ a / i.
+\ 5img class="anchor" src="icons/tick.png" id="le_div_times_m"\ 6theorem le_div_times_m: ∀a,i,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 i → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m →
+ (a \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 (m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 i)) \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 a \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 i.
 #a #i #m #posi #posm
-@(transitive_le ? ((a*m/i)/m))
-  [@monotonic_div /2/
-  |>eq_div_div_div_div // >div_times //
+@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6i)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m))
+  [@\ 5a href="cic:/matita/arithmetics/div_and_mod/monotonic_div.def(15)"\ 6monotonic_div\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/le_times_div_div_times.def(15)"\ 6le_times_div_div_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |>\ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_div.def(15)"\ 6eq_div_div_div_div\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6 //
   ]
 qed.
-
-(* serve ?
-theorem le_div_times_Sm: ∀a,i,m. O < i → O < m →
-a / i ≤ (a * S (m / i))/m.
-intros.
-apply (trans_le ? ((a * S (m/i))/((S (m/i))*i)))
-  [rewrite < (eq_div_div_div_times ? i)
-    [rewrite > lt_O_to_div_times
-      [apply le_n
-      |apply lt_O_S
-      ]
-    |apply lt_O_S
-    |assumption
-    ]
-  |apply le_times_to_le_div
-    [assumption
-    |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
-      [apply le_times_div_div_times.
-       rewrite > (times_n_O O).
-       apply lt_times
-        [apply lt_O_S
-        |assumption
-        ]
-      |rewrite > sym_times.
-       apply le_times_to_le_div2
-        [rewrite > (times_n_O O).
-         apply lt_times
-          [apply lt_O_S
-          |assumption
-          ]
-        |apply le_times_r.
-         apply lt_to_le.
-         apply lt_div_S.
-         assumption
-        ]
-      ]
-    ]
-  ]
-qed. *)