X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Fnat.ma;fp=weblib%2Farithmetics%2Fnat.ma;h=28248bdfce6b9bfbaf22f4a18462251075568666;hb=deff2f761d3e025908b6006c6fe3c07f1aa28d64;hp=8c3231ee16a7ff493019d859ea81e7ce412471a1;hpb=e81cff3104cd52f5a8d511b2802c42f7e1aa4d91;p=helm.git

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index 8c3231ee1..28248bdfc 100644
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -11,7 +11,7 @@
 
 include "basics/relations.ma".
 
-inductive nat : Type[0] ≝
+img class="anchor" src="icons/tick.png" id="nat"inductive nat : Type[0] ≝
   | O : nat
   | S : nat → nat.
   
@@ -19,37 +19,37 @@ interpretation "Natural numbers" 'N = nat.
 
 alias num (instance 0) = "natural number".
 
-definition pred ≝
+img class="anchor" src="icons/tick.png" id="pred"definition pred ≝
  λn. match n with [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | S p ⇒ p].
 
-theorem pred_Sn : ∀n.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n).
+img class="anchor" src="icons/tick.png" id="pred_Sn"theorem pred_Sn : ∀n.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n).
 // qed.
 
-theorem injective_S : a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a.
+img class="anchor" src="icons/tick.png" id="injective_S"theorem injective_S : a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a.
 // qed.
 
 (*
 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
 //. qed. *)
 
-theorem not_eq_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
+img class="anchor" src="icons/tick.png" id="not_eq_S"theorem not_eq_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ qed.
 
-definition not_zero: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
+img class="anchor" src="icons/tick.png" id="not_zero"definition not_zero: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
  λn: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. match n with [ O ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a | (S p) ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a ].
 
-theorem not_eq_O_S : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
+img class="anchor" src="icons/tick.png" id="not_eq_O_S"theorem not_eq_O_S : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
 #n @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #eqOS (change with (a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a)) >eqOS // qed.
 
-theorem not_eq_n_Sn: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
+img class="anchor" src="icons/tick.png" id="not_eq_n_Sn"theorem not_eq_n_Sn: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
 #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/ qed.
 
-theorem nat_case:
+img class="anchor" src="icons/tick.png" id="nat_case"theorem nat_case:
  ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop. 
   (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → P a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) → (∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → P (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) → P n.
 #n #P (elim n) /span class="autotactic"2span class="autotrace" trace /span/span/ qed.
 
-theorem nat_elim2 :
+img class="anchor" src="icons/tick.png" id="nat_elim2"theorem nat_elim2 :
  ∀R:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop.
   (∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a n) 
   → (∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a)
@@ -57,18 +57,18 @@ theorem nat_elim2 :
   → ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R n m.
 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /span class="autotactic"2span class="autotrace" trace /span/span/ qed.
 
-theorem decidable_eq_nat : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am).
+img class="anchor" src="icons/tick.png" id="decidable_eq_nat"theorem decidable_eq_nat : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am).
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n [ (cases n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a/span/span/ | #m #Hind (cases Hind) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/]
 qed. 
 
 (*************************** plus ******************************)
 
-let rec plus n m ≝ 
+img class="anchor" src="icons/tick.png" id="plus"let rec plus n m ≝ 
  match n with [ O ⇒ m | S p ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (plus p m) ].
 
 interpretation "natural plus" 'plus x y = (plus x y).
 
-theorem plus_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural plus" href="cic:/fakeuri.def(1)"+/an.
+img class="anchor" src="icons/tick.png" id="plus_O_n"theorem plus_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural plus" href="cic:/fakeuri.def(1)"+/an.
 // qed.
 
 (*
@@ -76,10 +76,10 @@ theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
 // qed.
 *)
 
-theorem plus_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="natural number" href="cic:/fakeuri.def(1)"0/a.
+img class="anchor" src="icons/tick.png" id="plus_n_O"theorem plus_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="natural number" href="cic:/fakeuri.def(1)"0/a.
 #n (elim n) normalize // qed.
 
-theorem plus_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
+img class="anchor" src="icons/tick.png" id="plus_n_Sm"theorem plus_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
 #n (elim n) normalize // qed.
 
 (*
@@ -92,16 +92,16 @@ theorem plus_n_1 : ∀n:nat. S n = n+1.
 // qed.
 *)
 
-theorem commutative_plus: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
+img class="anchor" src="icons/tick.png" id="commutative_plus"theorem commutative_plus: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
 #n (elim n) normalize // qed. 
 
-theorem associative_plus : a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
+img class="anchor" src="icons/tick.png" id="associative_plus"theorem associative_plus : a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
 #n (elim n) normalize // qed.
 
-theorem assoc_plus1: ∀a,b,c. c a title="natural plus" href="cic:/fakeuri.def(1)"+/a (b a title="natural plus" href="cic:/fakeuri.def(1)"+/a a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a a.
+img class="anchor" src="icons/tick.png" id="assoc_plus1"theorem assoc_plus1: ∀a,b,c. c a title="natural plus" href="cic:/fakeuri.def(1)"+/a (b a title="natural plus" href="cic:/fakeuri.def(1)"+/a a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a a.
 // qed. 
 
-theorem injective_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am).
+img class="anchor" src="icons/tick.png" id="injective_plus_r"theorem injective_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am).
 #n (elim n) normalize /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a/span/span/ qed.
 
 (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
@@ -115,43 +115,43 @@ theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
 
 (*************************** times *****************************)
 
-let rec times n m ≝ 
+img class="anchor" src="icons/tick.png" id="times"let rec times n m ≝ 
  match n with [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | S p ⇒ ma title="natural plus" href="cic:/fakeuri.def(1)"+/a(times p m) ].
 
 interpretation "natural times" 'times x y = (times x y).
 
-theorem times_Sn_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ma title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural times" href="cic:/fakeuri.def(1)"*/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="natural times" href="cic:/fakeuri.def(1)"*/am.
+img class="anchor" src="icons/tick.png" id="times_Sn_m"theorem times_Sn_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ma title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural times" href="cic:/fakeuri.def(1)"*/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="natural times" href="cic:/fakeuri.def(1)"*/am.
 // qed.
 
-theorem times_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural times" href="cic:/fakeuri.def(1)"*/an.
+img class="anchor" src="icons/tick.png" id="times_O_n"theorem times_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural times" href="cic:/fakeuri.def(1)"*/an.
 // qed.
 
-theorem times_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
+img class="anchor" src="icons/tick.png" id="times_n_O"theorem times_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
 #n (elim n) // qed.
 
-theorem times_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural times" href="cic:/fakeuri.def(1)"*/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m).
+img class="anchor" src="icons/tick.png" id="times_n_Sm"theorem times_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural times" href="cic:/fakeuri.def(1)"*/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m).
 #n (elim n) normalize // qed.
 
-theorem commutative_times : a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. 
+img class="anchor" src="icons/tick.png" id="commutative_times"theorem commutative_times : a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. 
 #n (elim n) normalize // qed. 
 
 (* variant sym_times : \forall n,m:nat. n*m = m*n \def
 symmetric_times. *)
 
-theorem distributive_times_plus : a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
+img class="anchor" src="icons/tick.png" id="distributive_times_plus"theorem distributive_times_plus : a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
 #n (elim n) normalize // qed.
 
-theorem distributive_times_plus_r :
+img class="anchor" src="icons/tick.png" id="distributive_times_plus_r"theorem distributive_times_plus_r :
   ∀a,b,c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. (ba title="natural plus" href="cic:/fakeuri.def(1)"+/ac)a title="natural times" href="cic:/fakeuri.def(1)"*/aa a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ba title="natural times" href="cic:/fakeuri.def(1)"*/aa a title="natural plus" href="cic:/fakeuri.def(1)"+/a ca title="natural times" href="cic:/fakeuri.def(1)"*/aa.
 // qed. 
 
-theorem associative_times: a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a.
+img class="anchor" src="icons/tick.png" id="associative_times"theorem associative_times: a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a.
 #n (elim n) normalize // qed.
 
-lemma times_times: ∀x,y,z. xa title="natural times" href="cic:/fakeuri.def(1)"*/a(ya title="natural times" href="cic:/fakeuri.def(1)"*/az) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ya title="natural times" href="cic:/fakeuri.def(1)"*/a(xa title="natural times" href="cic:/fakeuri.def(1)"*/az).
+img class="anchor" src="icons/tick.png" id="times_times"lemma times_times: ∀x,y,z. xa title="natural times" href="cic:/fakeuri.def(1)"*/a(ya title="natural times" href="cic:/fakeuri.def(1)"*/az) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ya title="natural times" href="cic:/fakeuri.def(1)"*/a(xa title="natural times" href="cic:/fakeuri.def(1)"*/az).
 // qed. 
 
-theorem times_n_1 : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural times" href="cic:/fakeuri.def(1)"*/a a title="natural number" href="cic:/fakeuri.def(1)"1/a.
+img class="anchor" src="icons/tick.png" id="times_n_1"theorem times_n_1 : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural times" href="cic:/fakeuri.def(1)"*/a a title="natural number" href="cic:/fakeuri.def(1)"1/a.
 #n // qed.
 
 (* ci servono questi risultati? 
@@ -182,7 +182,7 @@ qed.
 
 (******************** ordering relations ************************)
 
-inductive le (n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
+img class="anchor" src="icons/tick.png" id="le"inductive le (n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
   | le_n : le n n
   | le_S : ∀ m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. le n m → le n (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m).
 
@@ -190,7 +190,7 @@ 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: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+img class="anchor" src="icons/tick.png" id="lt"definition lt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a 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: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+img class="anchor" src="icons/tick.png" id="ge"definition ge: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 
 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
 
-definition gt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.ma title="natural 'less than'" href="cic:/fakeuri.def(1)"</an.
+img class="anchor" src="icons/tick.png" id="gt"definition gt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.ma title="natural 'less than'" href="cic:/fakeuri.def(1)"</an.
 
 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 : a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a.
+img class="anchor" src="icons/tick.png" id="transitive_le"theorem transitive_le : a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a.
 #a #b #c #leab #lebc (elim lebc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/
 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: a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a.
+img class="anchor" src="icons/tick.png" id="transitive_lt"theorem transitive_lt: a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a.
 #a #b #c #ltab #ltbc (elim ltbc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/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:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
+img class="anchor" src="icons/tick.png" id="le_S_S"theorem le_S_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
 #n #m #lenm (elim lenm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed.
 
-theorem le_O_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+img class="anchor" src="icons/tick.png" id="le_O_n"theorem le_O_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed.
 
-theorem le_n_Sn : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
+img class="anchor" src="icons/tick.png" id="le_n_Sn"theorem le_n_Sn : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed.
 
-theorem le_pred_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+img class="anchor" src="icons/tick.png" id="le_pred_n"theorem le_pred_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 #n (elim n) // qed.
 
-theorem monotonic_pred: a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a ? a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a.
+img class="anchor" src="icons/tick.png" id="monotonic_pred"theorem monotonic_pred: a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a ? a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a.
 #n #m #lenm (elim lenm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed.
 
-theorem le_S_S_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+img class="anchor" src="icons/tick.png" id="le_S_S_to_le"theorem le_S_S_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 (* demo *)
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed.
 
@@ -248,10 +248,14 @@ 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:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a m.
+img class="anchor" src="icons/tick.png" id="lt_to_not_zero"theorem lt_to_not_zero : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a m.
 #n #m #Hlt (elim Hlt) // qed.
 
 (* lt vs. le *)
+
+img class="anchor" src="icons/tick.png" id="lt_to_le"lemma lt_to_le: ∀n,m. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+#n #m #H @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a @H qed-.
+
 theorem not_le_Sn_O: ∀ n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
 #n @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Hlen0 @(a href="cic:/matita/arithmetics/nat/lt_to_not_zero.def(2)"lt_to_not_zero/a ?? Hlen0) qed.