commit by user utente1

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index 6fa6d57a8e78b130ae818438e644254019bee790..f14392e9363b16d8b82eea79a35fcc25eafc7ccc 100644 (file)
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -20,55 +20,55 @@ interpretation "Natural numbers" 'N = nat.
 alias num (instance 0) = "natural number".
 
 definition pred ≝
- λn. match n with [ O ⇒ O | S p ⇒ p].
+ λn. match n with [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 | S p ⇒ p].
 
-theorem pred_Sn : ∀n.n = pred (S n).
+theorem pred_Sn : ∀n.n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n).
 // qed.
 
-theorem injective_S : injective nat nat S.
+theorem injective_S : \ 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 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6.
 // qed.
 
 (*
 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
 //. qed. *)
 
-theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+theorem not_eq_S: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's non-equality" 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="leibnitz's non-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 m.
 /2/ qed.
 
-definition not_zero: nat → Prop ≝
- λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
+definition not_zero: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝
+ λn: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. match n with [ O ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 | (S p) ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 ].
 
-theorem not_eq_O_S : ∀n:nat. O ≠ S n.
-#n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
+theorem not_eq_O_S : ∀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="leibnitz's non-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.
+#n @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #eqOS (change with (\ 5a href="cic:/matita/arithmetics/nat/not_zero.def(1)"\ 6not_zero\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6)) >eqOS // qed.
 
-theorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
+theorem not_eq_n_Sn: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's non-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.
 #n (elim n) /2/ qed.
 
 theorem nat_case:
- ∀n:nat.∀P:nat → Prop. 
-  (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
+ ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.∀P:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop. 
+  (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 → P \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6) → (∀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/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m → P (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) → P n.
 #n #P (elim n) /2/ qed.
 
 theorem nat_elim2 :
- ∀R:nat → nat → Prop.
-  (∀n:nat. R O n) 
-  → (∀n:nat. R (S n) O)
-  → (∀n,m:nat. R n m → R (S n) (S m))
-  → ∀n,m:nat. R n m.
+ ∀R:\ 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 → Prop.
+  (∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. R \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 n) 
+  → (∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. R (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6)
+  → (∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. R n m → R (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m))
+  → ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. R n m.
 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
 
-theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
-@nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/]
+theorem decidable_eq_nat : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6m).
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/]
 qed. 
 
 (*************************** plus ******************************)
 
 let rec plus n m ≝ 
- match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
+ match n with [ O ⇒ m | S p ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (plus p m) ].
 
 interpretation "natural plus" 'plus x y = (plus x y).
 
-theorem plus_O_n: ∀n:nat. n = O+n.
+theorem plus_O_n: ∀n:\ 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/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n.
 // qed.
 
 (*
@@ -76,10 +76,10 @@ theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
 // qed.
 *)
 
-theorem plus_n_O: ∀n:nat. n = n+0.
+theorem plus_n_O: ∀n:\ 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 plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6.
 #n (elim n) normalize // qed.
 
-theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
+theorem plus_n_Sm : ∀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,2,0)"\ 6S\ 5/a\ 6 (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 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 m.
 #n (elim n) normalize // qed.
 
 (*
@@ -92,16 +92,16 @@ theorem plus_n_1 : ∀n:nat. S n = n+1.
 // qed.
 *)
 
-theorem commutative_plus: commutative ? plus.
+theorem commutative_plus: \ 5a href="cic:/matita/basics/relations/commutative.def(1)"\ 6commutative\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
 #n (elim n) normalize // qed. 
 
-theorem associative_plus : associative nat plus.
+theorem associative_plus : \ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
 #n (elim n) normalize // qed.
 
-theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
+theorem assoc_plus1: ∀a,b,c. c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (b \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 a) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 a.
 // qed. 
 
-theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
+theorem injective_plus_r: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 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.n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m).
 #n (elim n) normalize /3/ qed.
 
 (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
@@ -116,42 +116,42 @@ theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
 (*************************** times *****************************)
 
 let rec times n m ≝ 
- match n with [ O ⇒ O | S p ⇒ m+(times p m) ].
+ match n with [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 | S p ⇒ m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(times p m) ].
 
 interpretation "natural times" 'times x y = (times x y).
 
-theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
+theorem times_Sn_m: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. m\ 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\ 6m \ 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 times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m.
 // qed.
 
-theorem times_O_n: ∀n:nat. O = O*n.
+theorem times_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="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 title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n.
 // qed.
 
-theorem times_n_O: ∀n:nat. O = n*O.
+theorem times_n_O: ∀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="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 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,1,0)"\ 6O\ 5/a\ 6.
 #n (elim n) // qed.
 
-theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
+theorem times_n_Sm : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 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 m).
 #n (elim n) normalize // qed.
 
-theorem commutative_times : commutative nat times. 
+theorem commutative_times : \ 5a href="cic:/matita/basics/relations/commutative.def(1)"\ 6commutative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6. 
 #n (elim n) normalize // qed. 
 
 (* variant sym_times : \forall n,m:nat. n*m = m*n \def
 symmetric_times. *)
 
-theorem distributive_times_plus : distributive nat times plus.
+theorem distributive_times_plus : \ 5a href="cic:/matita/basics/relations/distributive.def(1)"\ 6distributive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
 #n (elim n) normalize // qed.
 
 theorem distributive_times_plus_r :
-  ∀a,b,c:nat. (b+c)*a = b*a + c*a.
+  ∀a,b,c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. (b\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6c)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6a.
 // qed. 
 
-theorem associative_times: associative nat times.
+theorem associative_times: \ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6.
 #n (elim n) normalize // qed.
 
-lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
+lemma times_times: ∀x,y,z. x\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(y\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(x\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6z).
 // qed. 
 
-theorem times_n_1 : ∀n:nat. n = n * 1.
+theorem times_n_1 : ∀n:\ 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 times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6.
 #n // qed.
 
 (* ci servono questi risultati? 
@@ -182,15 +182,15 @@ qed.
 
 (******************** ordering relations ************************)
 
-inductive le (n:nat) : nat → Prop ≝
+inductive le (n:\ 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 → Prop ≝
   | le_n : le n n
-  | le_S : ∀ m:nat. le n m → le n (S m).
+  | le_S : ∀ m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. le n m → le n (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m).
 
 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
 
 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
 
-definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
+definition lt: \ 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 → Prop ≝ λn,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
 
 interpretation "natural 'less than'" 'lt x y = (lt x y).
 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
@@ -198,16 +198,16 @@ interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
 (* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
 // qed. *)
 
-definition ge: nat → nat → Prop ≝ λn,m.m ≤ n.
+definition ge: \ 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 → Prop ≝ λn,m.m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
 
 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
 
-definition gt: nat → nat → Prop ≝ λn,m.m<n.
+definition gt: \ 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 → Prop ≝ λn,m.m\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6n.
 
 interpretation "natural 'greater than'" 'gt x y = (gt x y).
 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
 
-theorem transitive_le : transitive nat le.
+theorem transitive_le : \ 5a href="cic:/matita/basics/relations/transitive.def(2)"\ 6transitive\ 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.
 #a #b #c #leab #lebc (elim lebc) /2/
 qed.
 
@@ -215,29 +215,29 @@ qed.
 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
 \def transitive_le. *)
 
-theorem transitive_lt: transitive nat lt.
+theorem transitive_lt: \ 5a href="cic:/matita/basics/relations/transitive.def(2)"\ 6transitive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"\ 6lt\ 5/a\ 6.
 #a #b #c #ltab #ltbc (elim ltbc) /2/qed.
 
 (*
 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
 \def transitive_lt. *)
 
-theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
+theorem le_S_S: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" 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 '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 m.
 #n #m #lenm (elim lenm) /2/ qed.
 
-theorem le_O_n : ∀n:nat. O ≤ n.
+theorem le_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 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
 #n (elim n) /2/ qed.
 
-theorem le_n_Sn : ∀n:nat. n ≤ S n.
+theorem le_n_Sn : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 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.
 /2/ qed.
 
-theorem le_pred_n : ∀n:nat. pred n ≤ n.
+theorem le_pred_n : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
 #n (elim n) // qed.
 
-theorem monotonic_pred: monotonic ? le pred.
+theorem monotonic_pred: \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"\ 6le\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6.
 #n #m #lenm (elim lenm) /2/ qed.
 
-theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
+theorem le_S_S_to_le: ∀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,2,0)"\ 6S\ 5/a\ 6 n \ 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 m → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
 (* demo *)
 /2/ qed.
 
@@ -248,26 +248,26 @@ theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
 /2/ qed. *)
 
-theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
+theorem lt_to_not_zero : ∀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 → \ 5a href="cic:/matita/arithmetics/nat/not_zero.def(1)"\ 6not_zero\ 5/a\ 6 m.
 #n #m #Hlt (elim Hlt) // qed.
 
 (* lt vs. le *)
-theorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
-#n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
+theorem not_le_Sn_O: ∀ 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,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'neither less nor equal to'" 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 @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Hlen0 @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_zero.def(2)"\ 6lt_to_not_zero\ 5/a\ 6 ?? Hlen0) qed.
 
-theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
+theorem not_le_to_not_le_S_S: ∀ n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'neither less nor equal to'" 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 'neither less nor 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 m.
 /3/ qed.
 
-theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
+theorem not_le_S_S_to_not_le: ∀ 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,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'neither less nor 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 m → n \ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"\ 6≰\ 5/a\ 6 m.
 /3/ qed.
 
-theorem decidable_le: ∀n,m. decidable (n≤m).
-@nat_elim2 #n /2/ #m * /3/ qed.
+theorem decidable_le: ∀n,m. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (n\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m).
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 #n /2/ #m * /3/ qed.
 
-theorem decidable_lt: ∀n,m. decidable (n < m).
-#n #m @decidable_le  qed.
+theorem decidable_lt: ∀n,m. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m).
+#n #m @\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a\ 6  qed.
 
-theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
+theorem not_le_Sn_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,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"\ 6≰\ 5/a\ 6 n.
 #n (elim n) /2/ qed.
 
 (* this is le_S_S_to_le
@@ -275,38 +275,38 @@ theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
 /2/ qed.
 *)
 
-lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
+lemma le_gen: ∀P:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop.∀n.(∀i. i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → P i) → P n.
 /2/ qed.
 
-theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
-@nat_elim2 #n
- [#abs @False_ind /2/
+theorem not_le_to_lt: ∀n,m. n \ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"\ 6≰\ 5/a\ 6 m → m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n.
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 #n
+ [#abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/
  |/2/
- |#m #Hind #HnotleSS @le_S_S /3/
+ |#m #Hind #HnotleSS @\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 /3/
  ]
 qed.
 
-theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
+theorem lt_to_not_le: ∀n,m. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → m \ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"\ 6≰\ 5/a\ 6 n.
 #n #m #Hltnm (elim Hltnm) /3/ qed.
 
-theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
+theorem not_lt_to_le: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'not less than'" href="cic:/fakeuri.def(1)"\ 6≮\ 5/a\ 6 m → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
 /4/ qed.
 
-theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
-#n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
+theorem le_to_not_lt: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → m \ 5a title="natural 'not less than'" href="cic:/fakeuri.def(1)"\ 6≮\ 5/a\ 6 n.
+#n #m #H @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 /2/ (* /3/ *) qed.
 
 (* lt and le trans *)
 
-theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
+theorem lt_to_le_to_lt: ∀n,m,p:\ 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 → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p → n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p.
 #n #m #p #H #H1 (elim H1) /2/ qed.
 
-theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
+theorem le_to_lt_to_lt: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p → n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p.
 #n #m #p #H (elim H) /3/ qed.
 
-theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
+theorem lt_S_to_lt: ∀n,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 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 m.
 /2/ qed.
 
-theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
+theorem ltn_to_ltO: ∀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 → \ 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.
 /2/ qed.
 
 (*
@@ -320,12 +320,12 @@ apply (ltn_to_ltO (pred (S O)) (pred n) ?).
  ]
 qed. *)
 
-theorem lt_O_n_elim: ∀n:nat. O < n → 
-  ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
-#n (elim n) // #abs @False_ind /2/
+theorem lt_O_n_elim: ∀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 → 
+  ∀P:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop.(∀m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.P (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) → P n.
+#n (elim n) // #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/
 qed.
 
-theorem S_pred: ∀n. 0 < n → S(pred n) = n.
+theorem S_pred: ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 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,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 n) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
 #n #posn (cases posn) //
 qed.
 
@@ -356,12 +356,12 @@ qed.
 *)
 
 (* le to lt or eq *)
-theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
+theorem le_to_or_lt_eq: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" 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 m \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m.
 #n #m #lenm (elim lenm) /3/ qed.
 
 (* not eq *)
-theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
-#n #m #H @not_to_not /2/ qed.
+theorem lt_to_not_eq : ∀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="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 m.
+#n #m #H @\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 /2/ qed.
 
 (*not lt 
 theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
@@ -388,30 +388,30 @@ intro
 apply (not_le_Sn_n ? H3).
 qed. *)
 
-theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
-#n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
+theorem not_eq_to_le_to_lt: ∀n,m. n\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6m → n\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m → n\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6m.
+#n #m #Hneq #Hle cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 ?? Hle) //
 #Heq /3/ qed.
 (*
 nelim (Hneq Heq) qed. *)
 
 (* le elimination *)
-theorem le_n_O_to_eq : ∀n:nat. n ≤ O → O=n.
-#n (cases n) // #a  #abs @False_ind /2/ qed.
+theorem le_n_O_to_eq : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 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,1,0)"\ 6O\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6n.
+#n (cases n) // #a  #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed.
 
-theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
-#n (cases n) // #a #abs @False_ind /2/ qed. 
+theorem le_n_O_elim: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 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,1,0)"\ 6O\ 5/a\ 6 → ∀P: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 →Prop. P \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 → P n.
+#n (cases n) // #a #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed. 
 
-theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m → 
-∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
+theorem le_n_Sm_elim : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.n \ 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 m → 
+∀P:Prop. (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 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 m → P) → (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 m → P) → P.
 #n #m #Hle #P (elim Hle) /3/ qed.
 
 (* le and eq *)
 
-theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-@nat_elim2 /4/
+theorem le_to_le_to_eq: ∀n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m.
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 /4/
 qed. 
 
-theorem lt_O_S : ∀n:nat. O < S n.
+theorem lt_O_S : ∀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 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n.
 /2/ qed.
 
 (*
@@ -441,109 +441,109 @@ qed.
 
 (* well founded induction principles *)
 
-theorem nat_elim1 : ∀n:nat.∀P:nat → Prop. 
-(∀m.(∀p. p < m → P p) → P m) → P n.
+theorem nat_elim1 : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.∀P:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop. 
+(∀m.(∀p. p \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → P p) → P m) → P n.
 #n #P #H 
-cut (∀q:nat. q ≤ n → P q) /2/
+cut (∀q:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. q \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → P q) /2/
 (elim n) 
  [#q #HleO (* applica male *) 
-    @(le_n_O_elim ? HleO)
-    @H #p #ltpO @False_ind /2/ (* 3 *)
+    @(\ 5a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"\ 6le_n_O_elim\ 5/a\ 6 ? HleO)
+    @H #p #ltpO @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ (* 3 *)
  |#p #Hind #q #HleS 
-    @H #a #lta @Hind @le_S_S_to_le /2/
+    @H #a #lta @Hind @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 /2/
  ]
 qed.
 
 (* some properties of functions *)
 
-definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
+definition increasing ≝ λf:\ 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:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. f n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n).
 
-theorem increasing_to_monotonic: ∀f:nat → nat.
-  increasing f → monotonic nat lt f.
+theorem increasing_to_monotonic: ∀f:\ 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/increasing.def(2)"\ 6increasing\ 5/a\ 6 f → \ 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/lt.def(1)"\ 6lt\ 5/a\ 6 f.
 #f #incr #n #m #ltnm (elim ltnm) /2/
 qed.
 
-theorem le_n_fn: ∀f:nat → nat. 
-  increasing f → ∀n:nat. n ≤ f n.
+theorem le_n_fn: ∀f:\ 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/increasing.def(2)"\ 6increasing\ 5/a\ 6 f → ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 f n.
 #f #incr #n (elim n) /2/
 qed.
 
-theorem increasing_to_le: ∀f:nat → nat. 
-  increasing f → ∀m:nat.∃i.m ≤ f i.
+theorem increasing_to_le: ∀f:\ 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/increasing.def(2)"\ 6increasing\ 5/a\ 6 f → ∀m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6i.m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 f i.
 #f #incr #m (elim m) /2/#n * #a #lenfa
-@(ex_intro ?? (S a)) /2/
+@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 ?? (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 a)) /2/
 qed.
 
-theorem increasing_to_le2: ∀f:nat → nat. increasing f → 
-  ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
+theorem increasing_to_le2: ∀f:\ 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/increasing.def(2)"\ 6increasing\ 5/a\ 6 f → 
+  ∀m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. f \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6i. f i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i).
 #f #incr #m #lem (elim lem)
-  [@(ex_intro ? ? O) /2/
-  |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
-    [@(ex_intro ? ? a) % /2/ 
-    |@(ex_intro ? ? (S a)) % //
+  [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 ? ? \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6) /2/
+  |#n #len * #a * #len #ltnr (cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … ltnr)) #H
+    [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 ? ? a) % /2/ 
+    |@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 ? ? (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 a)) % //
     ]
   ]
 qed.
 
-theorem increasing_to_injective: ∀f:nat → nat.
-  increasing f → injective nat nat f.
-#f #incr #n #m cases(decidable_le n m)
-  [#lenm cases(le_to_or_lt_eq … lenm) //
-   #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq 
-   @increasing_to_monotonic //
-  |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq 
-   @lt_to_not_eq @increasing_to_monotonic /2/
+theorem increasing_to_injective: ∀f:\ 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/increasing.def(2)"\ 6increasing\ 5/a\ 6 f → \ 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 f.
+#f #incr #n #m cases(\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a\ 6 n m)
+  [#lenm cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … lenm) //
+   #lenm #eqf @\ 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 … eqf) @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"\ 6lt_to_not_eq\ 5/a\ 6 
+   @\ 5a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"\ 6increasing_to_monotonic\ 5/a\ 6 //
+  |#nlenm #eqf @\ 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 … eqf) @\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6 
+   @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"\ 6lt_to_not_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"\ 6increasing_to_monotonic\ 5/a\ 6 /2/
   ]
 qed.
 
 (*********************** monotonicity ***************************)
 theorem monotonic_le_plus_r: 
-∀n:nat.monotonic nat le (λm.n + m).
+∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 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.n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 m).
 #n #a #b (elim n) normalize //
-#m #H #leab @le_S_S /2/ qed.
+#m #H #leab @\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 /2/ qed.
 
 (*
 theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
 ≝ monotonic_le_plus_r. *)
 
 theorem monotonic_le_plus_l: 
-∀m:nat.monotonic nat le (λn.n + m).
+∀m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 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 (λn.n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 m).
 /2/ qed.
 
 (*
 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 \def monotonic_le_plus_l. *)
 
-theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2 
-→ n1 + m1 ≤ n2 + m2.
-#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
+theorem le_plus: ∀n1,n2,m1,m2:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n2  → m1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m2 
+→ n1 \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 m1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n2 \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 m2.
+#n1 #n2 #m1 #m2 #len #lem @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (n1\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m2))
 /2/ qed.
 
-theorem le_plus_n :∀n,m:nat. m ≤ n + m.
+theorem le_plus_n :∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 m.
 /2/ qed. 
 
-lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
+lemma le_plus_a: ∀a,n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 m.
 /2/ qed.
 
-lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
+lemma le_plus_b: ∀b,n,m. n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
 /2/ qed.
 
-theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
+theorem le_plus_n_r :∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 n.
 /2/ qed.
 
-theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
+theorem eq_plus_to_le: ∀n,m,p:\ 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\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
 // qed.
 
-theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
+theorem le_plus_to_le: ∀a,n,m. a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 m → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
 #a (elim a) normalize /3/ qed. 
 
-theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
+theorem le_plus_to_le_r: ∀a,n,m. n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6a → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
 /2/ qed. 
 
-(* plus & lt *)
+(* plus &amp; lt *)
 
 theorem monotonic_lt_plus_r: 
-∀n:nat.monotonic nat lt (λm.n+m).
+∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 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/lt.def(1)"\ 6lt\ 5/a\ 6 (λm.n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m).
 /2/ qed.
 
 (*
@@ -551,21 +551,21 @@ variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
 monotonic_lt_plus_r. *)
 
 theorem monotonic_lt_plus_l: 
-∀n:nat.monotonic nat lt (λm.m+n).
+∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 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/lt.def(1)"\ 6lt\ 5/a\ 6 (λm.m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n).
 /2/ qed.
 
 (*
 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
 monotonic_lt_plus_l. *)
 
-theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
+theorem lt_plus: ∀n,m,p,q:\ 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 → p \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q → n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 p \ 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 q.
 #n #m #p #q #ltnm #ltpq
-@(transitive_lt ? (n+q))/2/ qed.
+@(\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"\ 6transitive_lt\ 5/a\ 6 ? (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6q))/2/ qed.
 
-theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
+theorem lt_plus_to_lt_l :∀n,p,q:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n → p\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6q.
 /2/ qed.
 
-theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
+theorem lt_plus_to_lt_r :∀n,p,q:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6q → p\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6q.
 /2/ qed.
 
 (*
@@ -578,9 +578,9 @@ normalize napplyS le_plus // qed.
 
 (* times *)
 theorem monotonic_le_times_r: 
-∀n:nat.monotonic nat le (λm. n * m).
+∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 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. n \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 m).
 #n #x #y #lexy (elim n) normalize//(* lento /2/*)
-#a #lea @le_plus //
+#a #lea @\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"\ 6le_plus\ 5/a\ 6 //
 qed.
 
 (*
@@ -597,23 +597,23 @@ theorem monotonic_le_times_l:
 theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
 \def monotonic_le_times_l. *)
 
-theorem le_times: ∀n1,n2,m1,m2:nat. 
-n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
-#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) /2/
+theorem le_times: ∀n1,n2,m1,m2:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. 
+n1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n2  → m1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m2 → n1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n2\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m2.
+#n1 #n2 #m1 #m2 #len #lem @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (n1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m2)) /2/
 qed.
 
 (* interessante *)
-theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
+theorem lt_times_n: ∀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 n → m \ 5a title="natural 'less or equal to'" 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 #H /2/ qed.
 
 theorem le_times_to_le: 
-∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
-#a @nat_elim2 normalize
+∀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 a → a \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n \ 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\ 6 m → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
+#a @\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 normalize
   [//
   |#n #H1 #H2 
-     @(transitive_le ? (a*S n)) /2/
+     @(\ 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\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) /2/
   |#n #m #H #lta #le
-     @le_S_S @H /2/
+     @\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 @H /2/
   ]
 qed.
 
@@ -622,7 +622,7 @@ theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
 #n #m #posm #lenm  (* interessante *)
 applyS (le_plus n m) // qed. *)
 
-(* times & lt *)
+(* times &amp; lt *)
 (*
 theorem lt_O_times_S_S: ∀n,m:nat.O < (S n)*(S m).
 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
@@ -684,41 +684,41 @@ apply lt_plus.assumption.assumption.
 qed. *)
 
 theorem monotonic_lt_times_r: 
-  ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
+  ∀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/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/lt.def(1)"\ 6lt\ 5/a\ 6 (λt.(c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6t)).
 #c #posc #n #m #ltnm
 (elim ltnm) normalize
   [/2/ 
-  |#a #_ #lt1 @(transitive_le … lt1) //
+  |#a #_ #lt1 @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … lt1) //
   ]
 qed.
 
 theorem monotonic_lt_times_l: 
-  ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+  ∀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/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/lt.def(1)"\ 6lt\ 5/a\ 6 (λt.(t\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c)).
 /2/
 qed.
 
 theorem lt_to_le_to_lt_times: 
-∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
+∀n,m,p,q:\ 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 → p \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 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 times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p \ 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 #m #p #q #ltnm #lepq #posq
-@(le_to_lt_to_lt ? (n*q))
-  [@monotonic_le_times_r //
-  |@monotonic_lt_times_l //
+@(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"\ 6le_to_lt_to_lt\ 5/a\ 6 ? (n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q))
+  [@\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6 //
+  |@\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(9)"\ 6monotonic_lt_times_l\ 5/a\ 6 //
   ]
 qed.
 
-theorem lt_times:∀n,m,p,q:nat. n<m → p<q → n*p < m*q.
-#n #m #p #q #ltnm #ltpq @lt_to_le_to_lt_times/2/
+theorem lt_times:∀n,m,p,q:\ 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\ 6m → p\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6q → n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p \ 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 #m #p #q #ltnm #ltpq @\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(10)"\ 6lt_to_le_to_lt_times\ 5/a\ 6/2/
 qed.
 
 theorem lt_times_n_to_lt_l: 
-∀n,p,q:nat. p*n < q*n → p < q.
-#n #p #q #Hlt (elim (decidable_lt p q)) //
-#nltpq @False_ind @(absurd ? ? (lt_to_not_le ? ? Hlt))
-applyS monotonic_le_times_r /2/
+∀n,p,q:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. p\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n → p \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q.
+#n #p #q #Hlt (elim (\ 5a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"\ 6decidable_lt\ 5/a\ 6 p q)) //
+#nltpq @\ 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/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 ? ? Hlt))
+applyS \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6 /2/
 qed.
 
 theorem lt_times_n_to_lt_r: 
-∀n,p,q:nat. n*p < n*q → p < q.
+∀n,p,q:\ 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\ 6p \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q → p \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q.
 /2/ qed.
 
 (*
@@ -769,35 +769,35 @@ qed. *)
 
 let rec minus n m ≝ 
  match n with 
- [ O ⇒ O
+ [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
  | S p ⇒ 
        match m with
-         [ O ⇒ S p
+         [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 p
     | S q ⇒ minus p q ]].
         
 interpretation "natural minus" 'minus x y = (minus x y).
 
-theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
+theorem minus_S_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,2,0)"\ 6S\ 5/a\ 6 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m.
 // qed.
 
-theorem minus_O_n: ∀n:nat.O=O-n.
+theorem minus_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="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 title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6n.
 #n (cases n) // qed.
 
-theorem minus_n_O: ∀n:nat.n=n-O.
+theorem minus_n_O: ∀n:\ 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\ 6n\ 5a title="natural minus" 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 (cases n) // qed.
 
-theorem minus_n_n: ∀n:nat.O=n-n.
+theorem minus_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="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6n.
 #n (elim n) // qed.
 
-theorem minus_Sn_n: ∀n:nat. S O = (S n)-n.
+theorem minus_Sn_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,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 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 minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6n.
 #n (elim n) normalize // qed.
 
-theorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
+theorem minus_Sn_m: ∀m,n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m \ 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 minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m).
 (* qualcosa da capire qui 
 #n #m #lenm nelim lenm napplyS refl_eq. *)
-@nat_elim2 
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 
   [//
-  |#n #abs @False_ind /2/ 
+  |#n #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ 
   |#n #m #Hind #c applyS Hind /2/
   ]
 qed.
@@ -810,41 +810,41 @@ theorem not_eq_to_le_to_le_minus:
 napplyS (not_eq_to_le_to_lt n (S m) H H1)
 qed. *)
 
-theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
-@nat_elim2 normalize // qed.
+theorem eq_minus_S_pred: ∀n,m. 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) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6(n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m).
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 normalize // qed.
 
 theorem plus_minus:
-∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
-@nat_elim2 
+∀m,n,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → (n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m)\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p)\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m.
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 
   [//
-  |#n #p #abs @False_ind /2/
+  |#n #p #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/
   |normalize/3/
   ]
 qed.
 
-theorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
+theorem minus_plus_m_m: ∀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 plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m)\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m.
 /2/ qed.
 
-theorem plus_minus_m_m: ∀n,m:nat.
-  m ≤ n → n = (n-m)+m.
-#n #m #lemn @sym_eq /2/ qed.
+theorem plus_minus_m_m: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+  m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m)\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m.
+#n #m #lemn @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 /2/ qed.
 
-theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
+theorem le_plus_minus_m_m: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m)\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m.
 #n (elim n) // #a #Hind #m (cases m) // normalize #n/2/  
 qed.
 
-theorem minus_to_plus :∀n,m,p:nat.
-  m ≤ n → n-m = p → n = m+p.
-#n #m #p #lemn #eqp (applyS plus_minus_m_m) //
+theorem minus_to_plus :∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+  m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p → n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p.
+#n #m #p #lemn #eqp (applyS \ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6) //
 qed.
 
-theorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
-#n #m #p #eqp @sym_eq (applyS (minus_plus_m_m p m))
+theorem plus_to_minus :∀n,m,p:\ 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 m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p → n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p.
+#n #m #p #eqp @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 (applyS (\ 5a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"\ 6minus_plus_m_m\ 5/a\ 6 p m))
 qed.
 
-theorem minus_pred_pred : ∀n,m:nat. O < n → O < m → 
-pred n - pred m = n - m.
-#n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
+theorem minus_pred_pred : ∀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 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 → 
+\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 m.
+#n #m #posn #posm @(\ 5a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"\ 6lt_O_n_elim\ 5/a\ 6 n posn) @(\ 5a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"\ 6lt_O_n_elim\ 5/a\ 6 m posm) //.
 qed.
 
 
@@ -900,75 +900,75 @@ qed.
 (* monotonicity and galois *)
 
 theorem monotonic_le_minus_l: 
-∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
-@nat_elim2 #p #q
-  [#lePO @(le_n_O_elim ? lePO) //
+∀p,q,n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. q \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p → q\ 5a title="natural minus" 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 p\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6n.
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 #p #q
+  [#lePO @(\ 5a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"\ 6le_n_O_elim\ 5/a\ 6 ? lePO) //
   |//
   |#Hind #n (cases n) // #a #leSS @Hind /2/
   ]
 qed.
 
-theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
-#n #m #p #lep @transitive_le
-  [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
+theorem le_minus_to_plus: ∀n,m,p. n\ 5a title="natural minus" 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 p → n\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m.
+#n #m #p #lep @\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6
+  [|@\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"\ 6le_plus_minus_m_m\ 5/a\ 6 | @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"\ 6monotonic_le_plus_l\ 5/a\ 6 // ]
 qed.
 
-theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
-#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
+theorem le_minus_to_plus_r: ∀a,b,c. c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 c → a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b.
+#a #b #c #Hlecb #H >(\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 … Hlecb) /2/
 qed.
 
-theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
+theorem le_plus_to_minus: ∀n,m,p. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m → n\ 5a title="natural minus" 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 p.
 #n #m #p #lep /2/ qed.
 
-theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
-#a #b #c #H @(le_plus_to_le_r … b) /2/
+theorem le_plus_to_minus_r: ∀a,b,c. a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 c → a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 c \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6b.
+#a #b #c #H @(\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"\ 6le_plus_to_le_r\ 5/a\ 6 … b) /2/
 qed.
 
-theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
-#a #b #c #H @not_le_to_lt 
-@(not_to_not … (lt_to_not_le …H)) /2/
+theorem lt_minus_to_plus: ∀a,b,c. a \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 b \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b.
+#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 
+@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 …H)) /2/
 qed.
 
-theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
-#a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
-@lt_to_not_le //
+theorem lt_minus_to_plus_r: ∀a,b,c. a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 c → a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b.
+#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"\ 6le_plus_to_minus\ 5/a\ 6 …))
+@\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 //
 qed.
 
-theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
-#n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
+theorem lt_plus_to_minus: ∀n,m,p. m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m → n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p.
+#n #m #p #lenm #H normalize <\ 5a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"\ 6minus_Sn_m\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"\ 6le_plus_to_minus\ 5/a\ 6 //
 qed.
 
-theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
-#a #b #c #H @le_plus_to_minus_r //
+theorem lt_plus_to_minus_r: ∀a,b,c. a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 b.
+#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"\ 6le_plus_to_minus_r\ 5/a\ 6 //
 qed. 
 
 theorem monotonic_le_minus_r: 
-∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
-#p #q #n #lepq @le_plus_to_minus
-@(transitive_le … (le_plus_minus_m_m ? q)) /2/
+∀p,q,n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. q \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p → n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6p \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6q.
+#p #q #n #lepq @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"\ 6le_plus_to_minus\ 5/a\ 6
+@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"\ 6le_plus_minus_m_m\ 5/a\ 6 ? q)) /2/
 qed.
 
-theorem eq_minus_O: ∀n,m:nat.
-  n ≤ m → n-m = O.
-#n #m #lenm @(le_n_O_elim (n-m)) /2/
+theorem eq_minus_O: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+  n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m \ 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 #lenm @(\ 5a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"\ 6le_n_O_elim\ 5/a\ 6 (n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m)) /2/
 qed.
 
-theorem distributive_times_minus: distributive ? times minus.
+theorem distributive_times_minus: \ 5a href="cic:/matita/basics/relations/distributive.def(1)"\ 6distributive\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/minus.fix(0,0,1)"\ 6minus\ 5/a\ 6.
 #a #b #c
-(cases (decidable_lt b c)) #Hbc
- [> eq_minus_O /2/ >eq_minus_O // 
-  @monotonic_le_times_r /2/
- |@sym_eq (applyS plus_to_minus) <distributive_times_plus 
-  @eq_f (applyS plus_minus_m_m) /2/
+(cases (\ 5a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"\ 6decidable_lt\ 5/a\ 6 b c)) #Hbc
+ [> \ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"\ 6eq_minus_O\ 5/a\ 6 /2/ >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"\ 6eq_minus_O\ 5/a\ 6 // 
+  @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6 /2/
+ |@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 (applyS \ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"\ 6plus_to_minus\ 5/a\ 6) <\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"\ 6distributive_times_plus\ 5/a\ 6 
+  @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 (applyS \ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6) /2/
 qed.
 
-theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
+theorem minus_plus: ∀n,m,p. n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p).
 #n #m #p 
-cases (decidable_le (m+p) n) #Hlt
-  [@plus_to_minus @plus_to_minus <associative_plus
-   @minus_to_plus //
-  |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
-   #H >eq_minus_O /2/ >eq_minus_O // 
+cases (\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a\ 6 (m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p) n) #Hlt
+  [@\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"\ 6plus_to_minus\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"\ 6plus_to_minus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6
+   @\ 5a href="cic:/matita/arithmetics/nat/minus_to_plus.def(8)"\ 6minus_to_plus\ 5/a\ 6 //
+  |cut (n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6p) [@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_n_Sn.def(1)"\ 6le_n_Sn\ 5/a\ 6 …)) @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 //]
+   #H >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"\ 6eq_minus_O\ 5/a\ 6 /2/ >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"\ 6eq_minus_O\ 5/a\ 6 // 
   ]
 qed.
 
@@ -978,11 +978,11 @@ theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
 >associative_plus <plus_minus_m_m //
 qed.  *)
 
-theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
-  p+(n-m) = n-(m-p).
+theorem minus_minus: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. p \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n →
+  p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(m\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6p).
 #n #m #p #lepm #lemn
-@sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
-<commutative_plus <plus_minus_m_m //
+@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"\ 6plus_to_minus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 //
+<\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 //
 qed.
 
 (*********************** boolean arithmetics ********************) 
@@ -990,67 +990,67 @@ include "basics/bool.ma".
 
 let rec eqb n m ≝ 
 match n with 
-  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 
-  | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
+  [ O ⇒ match m with [ O ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | S q ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6] 
+  | S p ⇒ match m with [ O ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 | S q ⇒ eqb p q]
   ].
 
-theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
-(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 
-@nat_elim2 
+theorem eqb_elim : ∀ n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
+(n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6m → (P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6)) → (n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 m → (P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6)) → (P (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n m)). 
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 
   [#n (cases n) normalize /3/ 
   |normalize /3/
   |normalize /4/ 
   ] 
 qed.
 
-theorem eqb_n_n: ∀n. eqb n n = true.
+theorem eqb_n_n: ∀n. \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 #n (elim n) normalize // qed. 
 
-theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
-#n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed.
+theorem eqb_true_to_eq: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m.
+#n #m @(\ 5a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"\ 6eqb_elim\ 5/a\ 6 n m) // #_ #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed.
 
-theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
-#n #m @(eqb_elim n m) /2/ qed.
+theorem eqb_false_to_not_eq: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 m.
+#n #m @(\ 5a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"\ 6eqb_elim\ 5/a\ 6 n m) /2/ qed.
 
-theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
+theorem eq_to_eqb_true: ∀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 m → \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 // qed.
 
-theorem not_eq_to_eqb_false: ∀n,m:nat.
-  n ≠  m → eqb n m = false.
-#n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed.
+theorem not_eq_to_eqb_false: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+  n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6  m → \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#n #m #noteq @\ 5a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"\ 6eqb_elim\ 5/a\ 6// #Heq @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed.
 
 let rec leb n m ≝ 
 match n with 
-    [ O ⇒ true
+    [ O ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
     | (S p) ⇒
        match m with 
-        [ O ⇒ false
+        [ O ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
              | (S q) ⇒ leb p q]].
 
-theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop. 
-(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
-@nat_elim2 normalize
+theorem leb_elim: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. ∀P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop. 
+(n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (n \ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"\ 6≰\ 5/a\ 6 m → P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → P (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m).
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 normalize
   [/2/
   |/3/
   |#n #m #Hind #P #Pt #Pf @Hind
-    [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ]
+    [#lenm @Pt @\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 // |#nlenm @Pf /2/ ]
   ]
 qed.
 
-theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
-#n #m @leb_elim // #_ #abs @False_ind /2/ qed.
+theorem leb_true_to_le:∀n,m.\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
+#n #m @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 // #_ #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed.
 
 theorem leb_false_to_not_le:∀n,m.
-  leb n m = false → n ≰ m.
-#n #m @leb_elim // #_ #abs @False_ind /2/ qed.
+  \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → n \ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"\ 6≰\ 5/a\ 6 m.
+#n #m @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 // #_ #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed.
 
-theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
-#n #m @leb_elim // #H #H1 @False_ind /2/ qed.
+theorem le_to_leb_true: ∀n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#n #m @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 // #H #H1 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed.
 
-theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false.
-#n #m @leb_elim // #H #H1 @False_ind /2/ qed.
+theorem not_le_to_leb_false: ∀n,m. n \ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"\ 6≰\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#n #m @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 // #H #H1 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed.
 
-theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
+theorem lt_to_leb_false: ∀n,m. m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
 /3/ qed.
 
 (* serve anche ltb? 
@@ -1079,41 +1079,40 @@ theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
 qed. *)
 
 (* min e max *)
-definition min: nat →nat →nat ≝
-λn.λm. if_then_else ? (leb n m) n m.
+definition min: \ 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. \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m) n m.
 
-definition max: nat →nat →nat ≝
-λn.λm. if_then_else ? (leb n m) m n.
+definition max: \ 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. \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m) m n.
 
-lemma commutative_min: commutative ? min.
-#n #m normalize @leb_elim 
-  [@leb_elim normalize /2/
-  |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
+lemma commutative_min: \ 5a href="cic:/matita/basics/relations/commutative.def(1)"\ 6commutative\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/min.def(2)"\ 6min\ 5/a\ 6.
+#n #m normalize @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 
+  [@\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 normalize /2/
+  |#notle >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 …) // @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) /2/
   ] qed.
 
-lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
-#i #n #m normalize @leb_elim normalize /2/ qed. 
+lemma le_minr: ∀i,n,m. i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/min.def(2)"\ 6min\ 5/a\ 6 n m → i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
+#i #n #m normalize @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 normalize /2/ qed. 
 
-lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
+lemma le_minl: ∀i,n,m. i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/min.def(2)"\ 6min\ 5/a\ 6 n m → i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
 /2/ qed.
 
-lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
-#i #n #m #lein #leim normalize (cases (leb n m)) 
+lemma to_min: ∀i,n,m. i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/min.def(2)"\ 6min\ 5/a\ 6 n m.
+#i #n #m #lein #leim normalize (cases (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m)) 
 normalize // qed.
 
-lemma commutative_max: commutative ? max.
-#n #m normalize @leb_elim 
-  [@leb_elim normalize /2/
-  |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
+lemma commutative_max: \ 5a href="cic:/matita/basics/relations/commutative.def(1)"\ 6commutative\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6.
+#n #m normalize @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 
+  [@\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 normalize /2/
+  |#notle >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 …) // @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) /2/
   ] qed.
 
-lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
-#i #n #m normalize @leb_elim normalize /2/ qed. 
+lemma le_maxl: ∀i,n,m. \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i.
+#i #n #m normalize @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 normalize /2/ qed. 
 
-lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
+lemma le_maxr: ∀i,n,m. \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i.
 /2/ qed.
 
-lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
-#i #n #m #leni #lemi normalize (cases (leb n m)) 
+lemma to_max: ∀i,n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i.
+#i #n #m #leni #lemi normalize (cases (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m)) 
 normalize // qed.
-