commit by user utente1

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index f14392e9363b16d8b82eea79a35fcc25eafc7ccc..ef8da2f1921c2d3f0510765e8b62f6306b49e8ab 100644 (file)
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -389,7 +389,7 @@ apply (not_le_Sn_n ? H3).
 qed. *)
 
 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) //
+#n #m #Hneq #Hle cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"\ 6le_to_or_lt_eq\ 5/a\ 6 ?? Hle) //
 #Heq /3/ qed.
 (*
 nelim (Hneq Heq) qed. *)
@@ -478,7 +478,7 @@ theorem increasing_to_le2: ∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0
   ∀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)
   [@(\ 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
+  |#n #len * #a * #len #ltnr (cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"\ 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)) % //
     ]
@@ -488,7 +488,7 @@ qed.
 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 cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"\ 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 
@@ -700,14 +700,14 @@ qed.
 theorem lt_to_le_to_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\ 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
-@(\ 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/le_to_lt_to_lt.def(5)"\ 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 //
+  |@\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"\ 6monotonic_lt_times_l\ 5/a\ 6 //
   ]
 qed.
 
 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/
+#n #m #p #q #ltnm #ltpq @\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"\ 6lt_to_le_to_lt_times\ 5/a\ 6\ 5span style="text-decoration: underline;"\ 6 \ 5/span\ 6/2/
 qed.
 
 theorem lt_times_n_to_lt_l: 
@@ -811,7 +811,8 @@ napplyS (not_eq_to_le_to_lt n (S m) H H1)
 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.
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 normalize //
+qed.
 
 theorem plus_minus:
 ∀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.
@@ -844,7 +845,7 @@ qed.
 
 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) //.
+#n #m #posn #posm @(\ 5a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(7)"\ 6lt_O_n_elim\ 5/a\ 6 n posn) @(\ 5a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(7)"\ 6lt_O_n_elim\ 5/a\ 6 m posm) //.
 qed.
 
 
@@ -910,7 +911,7 @@ qed.
 
 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 // ]
+  [|@\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(8)"\ 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 \ 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.
@@ -930,22 +931,22 @@ theorem lt_minus_to_plus: ∀a,b,c. a \ 5a title="natural minus" href="cic:/fakeur
 qed.
 
 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 …))
+#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(9)"\ 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 \ 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 //
+#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(9)"\ 6le_plus_to_minus\ 5/a\ 6 //
 qed.
 
 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 //
+#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(9)"\ 6le_plus_to_minus_r\ 5/a\ 6 //
 qed. 
 
 theorem monotonic_le_minus_r: 
 ∀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/
+#p #q #n #lepq @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"\ 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(8)"\ 6le_plus_minus_m_m\ 5/a\ 6 ? q)) /2/
 qed.
 
 theorem eq_minus_O: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
@@ -956,7 +957,7 @@ qed.
 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 (\ 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/eq_minus_O.def(11)"\ 6eq_minus_O\ 5/a\ 6 /2/ >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"\ 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/
@@ -968,7 +969,7 @@ cases (\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a
   [@\ 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 // 
+   #H >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"\ 6eq_minus_O\ 5/a\ 6 /2/ >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"\ 6eq_minus_O\ 5/a\ 6 // 
   ]
 qed.
 
@@ -1115,4 +1116,4 @@ lemma le_maxr: ∀i,n,m. \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a
 
 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.
+normalize // qed.
\ No newline at end of file

diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma
index b31db23d7ffffa2e8e6888311194c70ce73b3029..3081fa96b05d8d5a3c966372a9b609b243afcf34 100644 (file)
--- a/weblib/basics/relations.ma
+++ b/weblib/basics/relations.ma
@@ -15,27 +15,27 @@ include "basics/logic.ma".
 definition relation : Type[0] → Type[0]
 ≝ λA.A→A→Prop. 
 
-definition reflexive: ∀A.∀R :relation A.Prop
+definition reflexive: ∀A.∀R :\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
 ≝ λA.λR.∀x:A.R x x.
 
-definition symmetric: ∀A.∀R: relation A.Prop
+definition symmetric: ∀A.∀R: \ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
 ≝ λA.λR.∀x,y:A.R x y → R y x.
 
-definition transitive: ∀A.∀R:relation A.Prop
+definition transitive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 
-definition irreflexive: ∀A.∀R:relation A.Prop
-≝ λA.λR.∀x:A.¬(R x x).
+definition irreflexive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λR.∀x:A.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(R x x).
 
-definition cotransitive: ∀A.∀R:relation A.Prop
-≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
+definition cotransitive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 R z y.
 
-definition tight_apart: ∀A.∀eq,ap:relation A.Prop
-≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
-(eq x y → ¬(ap x y)).
+definition tight_apart: ∀A.∀eq,ap:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λeq,ap.∀x,y:A. (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y) → eq x y) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6
+(eq x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y)).
 
-definition antisymmetric: ∀A.∀R:relation A.Prop
-≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
+definition antisymmetric: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λR.∀x,y:A. R x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(R y x).
 
 (********** functions **********)
 
@@ -45,19 +45,19 @@ definition compose ≝
 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
 
 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
-≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
+≝ λA,B.λf.∀x,y:A.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y → x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y.
 
 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
-≝λA,B.λf.∀z:B.∃x:A.z = f x.
+≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6x:A.z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
 
 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop 
-≝ λA.λf.∀x,y.f x y = f y x.
+≝ λA.λf.∀x,y.f x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y x.
 
 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
-≝ λA,B.λf.∀x,y.f x y = f y x.
+≝ λA,B.λf.∀x,y.f x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y x.
 
 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
-≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
+≝ λA.λf.∀x,y,z.f (f x y) z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x (f y z).
 
 (* functions and relations *)
 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
@@ -66,25 +66,25 @@ definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
 
 (* functions and functions *)
 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
-≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
+≝ λA.λf,g.∀x,y,z:A. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g (f x y) (f x z).
 
 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
-≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
+≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g (f x y) (f x z).
 
 lemma injective_compose : ∀A,B,C,f,g.
-injective A B f → injective B C g → injective A C (λx.g (f x)).
+\ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A B f → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 B C g → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A C (λx.g (f x)).
 /3/; qed.
 
 (* extensional equality *)
 
 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
-λA.λP,Q.∀a.iff (P a) (Q a).
+λA.λP,Q.∀a.\ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (P a) (Q a).
 
 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
-λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
+λA,B.λR,S.∀a.∀b.\ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (R a b) (S a b).
 
 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
-λA,B.λf,g.∀a.f a = g a.
+λA,B.λf,g.∀a.f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g a.
 
 notation " x \eqP y " non associative with precedence 45 
 for @{'eqP A $x $y}.
@@ -102,5 +102,4 @@ notation " f \eqF g " non associative with precedence 45
 for @{'eqF ? ? f g}.
 
 interpretation "functional extentional equality" 
-'eqF A B f g = (exteqF A B f g).
-
+'eqF A B f g = (exteqF A B f g).
\ No newline at end of file