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

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index d45b0121b..28248bdfc 100644
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -252,22 +252,26 @@ theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
 #n #m #Hlt (elim Hlt) // qed.
 
 (* lt vs. le *)
-img class="anchor" src="icons/tick.png" id="not_le_Sn_O"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.
+
+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.
 
-img class="anchor" src="icons/tick.png" id="not_le_to_not_le_S_S"theorem not_le_to_not_le_S_S: ∀ n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'neither less nor 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 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
+theorem not_le_to_not_le_S_S: ∀ n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'neither less nor 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 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="not_le_S_S_to_not_le"theorem not_le_S_S_to_not_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 'neither less nor 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 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m.
+theorem not_le_S_S_to_not_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 'neither less nor 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 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m.
 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="decidable_le"theorem decidable_le: ∀n,m. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am).
+theorem decidable_le: ∀n,m. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am).
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #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/ #m * /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_le_to_not_le_S_S.def(5)"not_le_to_not_le_S_S/a, a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="decidable_lt"theorem decidable_lt: ∀n,m. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m).
+theorem decidable_lt: ∀n,m. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m).
 #n #m @a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a  qed.
 
-img class="anchor" src="icons/tick.png" id="not_le_Sn_n"theorem not_le_Sn_n: ∀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 n.
+theorem not_le_Sn_n: ∀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 n.
 #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"not_le_to_not_le_S_S/a/span/span/ qed.
 
 (* this is le_S_S_to_le
@@ -275,10 +279,10 @@ theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
 /2/ qed.
 *)
 
-img class="anchor" src="icons/tick.png" id="le_gen"lemma le_gen: ∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop.∀n.(∀i. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → P i) → P n.
+lemma le_gen: ∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop.∀n.(∀i. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → P i) → P n.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="not_le_to_lt"theorem not_le_to_lt: ∀n,m. n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n.
+theorem not_le_to_lt: ∀n,m. n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n.
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n
  [#abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
  |/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/
@@ -286,132 +290,70 @@ theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
  ]
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_to_not_le"theorem lt_to_not_le: ∀n,m. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → m a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a n.
+theorem lt_to_not_le: ∀n,m. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → m a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a n.
 #n #m #Hltnm (elim Hltnm) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="not_lt_to_le"theorem not_lt_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'not less than'" href="cic:/fakeuri.def(1)"≮/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+theorem not_lt_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'not less than'" href="cic:/fakeuri.def(1)"≮/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 /span class="autotactic"4span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a, a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_to_not_lt"theorem le_to_not_lt: ∀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 → m a title="natural 'not less than'" href="cic:/fakeuri.def(1)"≮/a n.
+theorem le_to_not_lt: ∀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 → m a title="natural 'not less than'" href="cic:/fakeuri.def(1)"≮/a n.
 #n #m #H @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ (* /3/ *) qed.
 
 (* lt and le trans *)
 
-img class="anchor" src="icons/tick.png" id="lt_to_le_to_lt"theorem lt_to_le_to_lt: ∀n,m,p: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 → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p.
+theorem lt_to_le_to_lt: ∀n,m,p: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 → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p.
 #n #m #p #H #H1 (elim H1) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_to_lt_to_lt"theorem le_to_lt_to_lt: ∀n,m,p: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 → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p.
+theorem le_to_lt_to_lt: ∀n,m,p: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 → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p.
 #n #m #p #H (elim H) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="lt_S_to_lt"theorem lt_S_to_lt: ∀n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m.
+theorem lt_S_to_lt: ∀n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="ltn_to_ltO"theorem ltn_to_ltO: ∀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/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m.
+theorem ltn_to_ltO: ∀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/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a/span/span/ qed.
 
-(*
-theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
-(S O) \lt n \to O \lt (pred n).
-intros.
-apply (ltn_to_ltO (pred (S O)) (pred n) ?).
- apply (lt_pred (S O) n)
- [ apply (lt_O_S O) 
- | assumption
- ]
-qed. *)
-
-img class="anchor" src="icons/tick.png" id="lt_O_n_elim"theorem lt_O_n_elim: ∀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 than'" href="cic:/fakeuri.def(1)"</a n → 
+theorem lt_O_n_elim: ∀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 than'" href="cic:/fakeuri.def(1)"</a n → 
   ∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop.(∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.P (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) → P n.
 #n (elim n) // #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="S_pred"theorem S_pred: ∀n. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
+theorem S_pred: ∀n. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
 #n #posn (cases posn) //
 qed.
 
-(*
-theorem lt_pred: \forall n,m. 
-  O < n \to n < m \to pred n < pred m. 
-apply nat_elim2
-  [intros.apply False_ind.apply (not_le_Sn_O ? H)
-  |intros.apply False_ind.apply (not_le_Sn_O ? H1)
-  |intros.simplify.unfold.apply le_S_S_to_le.assumption
-  ]
-qed.
-
-theorem le_pred_to_le:
- ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
-intros 2
-elim n
-[ apply le_O_n
-| simplify in H2
-  rewrite > (S_pred m)
-  [ apply le_S_S
-    assumption
-  | assumption
-  ]
-].
-qed.
-
-*)
-
 (* le to lt or eq *)
-img class="anchor" src="icons/tick.png" id="le_to_or_lt_eq"theorem le_to_or_lt_eq: ∀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 → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m a title="logical or" href="cic:/fakeuri.def(1)"∨/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
+theorem le_to_or_lt_eq: ∀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 → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m a title="logical or" href="cic:/fakeuri.def(1)"∨/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
 #n #m #lenm (elim lenm) /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/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed.
 
 (* not eq *)
-img class="anchor" src="icons/tick.png" id="lt_to_not_eq"theorem lt_to_not_eq : ∀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 → n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m.
+theorem lt_to_not_eq : ∀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 → n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m.
 #n #m #H @a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a, a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/ qed.
 
-(*not lt 
-theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
-intros.
-unfold Not.
-intros.
-rewrite > H in H1.
-apply (lt_to_not_eq b b)
-[ assumption
-| reflexivity
-]
-qed. 
-
-theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
-intros
-unfold Not
-intro
-unfold lt in H
-unfold lt in H1
-generalize in match (le_S_S ? ? H)
-intro
-generalize in match (transitive_le ? ? ? H2 H1)
-intro
-apply (not_le_Sn_n ? H3).
-qed. *)
-
-img class="anchor" src="icons/tick.png" id="not_eq_to_le_to_lt"theorem not_eq_to_le_to_lt: ∀n,m. na title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/am → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am → na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am.
+theorem not_eq_to_le_to_lt: ∀n,m. na title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/am → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am → na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am.
 #n #m #Hneq #Hle cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a ?? Hle) //
 #Heq /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/ qed.
 (*
 nelim (Hneq Heq) qed. *)
 
 (* le elimination *)
-img class="anchor" src="icons/tick.png" id="le_n_O_to_eq"theorem le_n_O_to_eq : ∀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,1,0)"O/a → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/an.
+theorem le_n_O_to_eq : ∀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,1,0)"O/a → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/an.
 #n (cases n) // #a  #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_n_O_elim"theorem le_n_O_elim: ∀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,1,0)"O/a → ∀P: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a →Prop. P a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → P n.
+theorem le_n_O_elim: ∀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,1,0)"O/a → ∀P: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a →Prop. P a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → P n.
 #n (cases n) // #a #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. 
 
-img class="anchor" src="icons/tick.png" id="le_n_Sm_elim"theorem le_n_Sm_elim : ∀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 a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → 
+theorem le_n_Sm_elim : ∀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 a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → 
 ∀P:Prop. (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 → P) → (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → P) → P.
 #n #m #Hle #P (elim Hle) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ qed.
 
 (* le and eq *)
 
-img class="anchor" src="icons/tick.png" id="le_to_le_to_eq"theorem le_to_le_to_eq: ∀n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
+theorem le_to_le_to_eq: ∀n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a /span class="autotactic"4span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/arithmetics/nat/le_n_O_to_eq.def(4)"le_n_O_to_eq/a, a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/
 qed. 
 
-img class="anchor" src="icons/tick.png" id="lt_O_S"theorem lt_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="natural 'less than'" href="cic:/fakeuri.def(1)"</a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
+theorem lt_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="natural 'less than'" 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/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/ qed.
 
 (*
@@ -441,7 +383,7 @@ qed.
 
 (* well founded induction principles *)
 
-img class="anchor" src="icons/tick.png" id="nat_elim1"theorem nat_elim1 : ∀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. 
+theorem nat_elim1 : ∀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. 
 (∀m.(∀p. p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → P p) → P m) → P n.
 #n #P #H 
 cut (∀q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → P q) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/
@@ -456,25 +398,25 @@ qed.
 
 (* some properties of functions *)
 
-img class="anchor" src="icons/tick.png" id="increasing"definition increasing ≝ λf: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. ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. f n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n).
+definition increasing ≝ λf: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. ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. f n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n).
 
-img class="anchor" src="icons/tick.png" id="increasing_to_monotonic"theorem increasing_to_monotonic: ∀f: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.
+theorem increasing_to_monotonic: ∀f: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/increasing.def(2)"increasing/a f → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/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 f.
 #f #incr #n #m #ltnm (elim ltnm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="le_n_fn"theorem le_n_fn: ∀f: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. 
+theorem le_n_fn: ∀f: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/increasing.def(2)"increasing/a f → ∀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 f n.
 #f #incr #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="increasing_to_le"theorem increasing_to_le: ∀f: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. 
+theorem increasing_to_le: ∀f: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/increasing.def(2)"increasing/a f → ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a title="exists" href="cic:/fakeuri.def(1)"∃/ai.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a f i.
 #f #incr #m (elim m) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a/span/span/#n * #a #lenfa
 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ?? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="increasing_to_le2"theorem increasing_to_le2: ∀f: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/increasing.def(2)"increasing/a f → 
+theorem increasing_to_le2: ∀f: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/increasing.def(2)"increasing/a f → 
   ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. f a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a title="exists" href="cic:/fakeuri.def(1)"∃/ai. f i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="logical and" href="cic:/fakeuri.def(1)"∧/a m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i).
 #f #incr #m #lem (elim lem)
   [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/
@@ -485,7 +427,7 @@ qed.
   ]
 qed.
 
-img class="anchor" src="icons/tick.png" id="increasing_to_injective"theorem increasing_to_injective: ∀f: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.
+theorem increasing_to_injective: ∀f: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/increasing.def(2)"increasing/a f → 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 f.
 #f #incr #n #m cases(a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a n m)
   [#lenm cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lenm) //
@@ -497,7 +439,7 @@ qed.
 qed.
 
 (*********************** monotonicity ***************************)
-img class="anchor" src="icons/tick.png" id="monotonic_le_plus_r"theorem monotonic_le_plus_r: 
+theorem monotonic_le_plus_r: 
 ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/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 (λm.n a title="natural plus" href="cic:/fakeuri.def(1)"+/a m).
 #n #a #b (elim n) normalize //
 #m #H #leab @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a /span class="autotactic"2span class="autotrace" trace /span/span/ qed.
@@ -506,7 +448,7 @@ qed.
 theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
 ≝ monotonic_le_plus_r. *)
 
-img class="anchor" src="icons/tick.png" id="monotonic_le_plus_l"theorem monotonic_le_plus_l: 
+theorem monotonic_le_plus_l: 
 ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/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 (λn.n a title="natural plus" href="cic:/fakeuri.def(1)"+/a m).
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/ qed.
 
@@ -514,35 +456,35 @@ theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 \def monotonic_le_plus_l. *)
 
-img class="anchor" src="icons/tick.png" id="le_plus"theorem le_plus: ∀n1,n2,m1,m2:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2  → m1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m2 
+theorem le_plus: ∀n1,n2,m1,m2:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2  → m1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m2 
 → n1 a title="natural plus" href="cic:/fakeuri.def(1)"+/a m1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2 a title="natural plus" href="cic:/fakeuri.def(1)"+/a m2.
 #n1 #n2 #m1 #m2 #len #lem @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (n1a title="natural plus" href="cic:/fakeuri.def(1)"+/am2))
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a, a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_plus_n"theorem le_plus_n :∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a m.
+theorem le_plus_n :∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a m.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a/span/span/ qed. 
 
-img class="anchor" src="icons/tick.png" id="le_plus_a"lemma le_plus_a: ∀a,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural plus" href="cic:/fakeuri.def(1)"+/a m.
+lemma le_plus_a: ∀a,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural plus" href="cic:/fakeuri.def(1)"+/a m.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_plus_b"lemma le_plus_b: ∀b,n,m. n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+lemma le_plus_b: ∀b,n,m. n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_plus_n_r"theorem le_plus_n_r :∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="natural plus" href="cic:/fakeuri.def(1)"+/a n.
+theorem le_plus_n_r :∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="natural plus" href="cic:/fakeuri.def(1)"+/a n.
 /span class="autotactic"2span class="autotrace" trace /span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="eq_plus_to_le"theorem eq_plus_to_le: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ama title="natural plus" href="cic:/fakeuri.def(1)"+/ap → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+theorem eq_plus_to_le: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ama title="natural plus" href="cic:/fakeuri.def(1)"+/ap → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 // qed.
 
-img class="anchor" src="icons/tick.png" id="le_plus_to_le"theorem le_plus_to_le: ∀a,n,m. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural plus" href="cic:/fakeuri.def(1)"+/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+theorem le_plus_to_le: ∀a,n,m. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural plus" href="cic:/fakeuri.def(1)"+/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 #a (elim a) normalize /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed. 
 
-img class="anchor" src="icons/tick.png" id="le_plus_to_le_r"theorem le_plus_to_le_r: ∀a,n,m. n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="natural plus" href="cic:/fakeuri.def(1)"+/aa → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+theorem le_plus_to_le_r: ∀a,n,m. n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="natural plus" href="cic:/fakeuri.def(1)"+/aa → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"le_plus_to_le/a/span/span/ qed. 
 
 (* plus &amp; lt *)
 
-img class="anchor" src="icons/tick.png" id="monotonic_lt_plus_r"theorem monotonic_lt_plus_r: 
+theorem monotonic_lt_plus_r: 
 ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/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 (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am).
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a/span/span/ qed.
 
@@ -550,7 +492,7 @@ theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
 monotonic_lt_plus_r. *)
 
-img class="anchor" src="icons/tick.png" id="monotonic_lt_plus_l"theorem monotonic_lt_plus_l: 
+theorem monotonic_lt_plus_l: 
 ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/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 (λm.ma title="natural plus" href="cic:/fakeuri.def(1)"+/an).
 (* /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a/span/span/ *) #n @a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a // qed.
 
@@ -558,14 +500,14 @@ monotonic_lt_plus_r. *)
 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
 monotonic_lt_plus_l. *)
 
-img class="anchor" src="icons/tick.png" id="lt_plus"theorem lt_plus: ∀n,m,p,q: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 → p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → n a title="natural plus" href="cic:/fakeuri.def(1)"+/a p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m a title="natural plus" href="cic:/fakeuri.def(1)"+/a q.
+theorem lt_plus: ∀n,m,p,q: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 → p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → n a title="natural plus" href="cic:/fakeuri.def(1)"+/a p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m a title="natural plus" href="cic:/fakeuri.def(1)"+/a q.
 #n #m #p #q #ltnm #ltpq
-@(a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a ? (na title="natural plus" href="cic:/fakeuri.def(1)"+/aq)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(5)"monotonic_lt_plus_l/a, a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/ qed.
+@(a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a ? (na title="natural plus" href="cic:/fakeuri.def(1)"+/aq))/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a, a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="lt_plus_to_lt_l"theorem lt_plus_to_lt_l :∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. pa title="natural plus" href="cic:/fakeuri.def(1)"+/an a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a qa title="natural plus" href="cic:/fakeuri.def(1)"+/an → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq.
+theorem lt_plus_to_lt_l :∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. pa title="natural plus" href="cic:/fakeuri.def(1)"+/an a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a qa title="natural plus" href="cic:/fakeuri.def(1)"+/an → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"le_plus_to_le/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="lt_plus_to_lt_r"theorem lt_plus_to_lt_r :∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a na title="natural plus" href="cic:/fakeuri.def(1)"+/aq → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq.
+theorem lt_plus_to_lt_r :∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a na title="natural plus" href="cic:/fakeuri.def(1)"+/aq → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"lt_plus_to_lt_l/a/span/span/ qed.
 
 (*
@@ -577,7 +519,7 @@ normalize napplyS le_plus // qed.
 *)
 
 (* times *)
-img class="anchor" src="icons/tick.png" id="monotonic_le_times_r"theorem monotonic_le_times_r: 
+theorem monotonic_le_times_r: 
 ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/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 (λm. n a title="natural times" href="cic:/fakeuri.def(1)"*/a m).
 #n #x #y #lexy (elim n) normalize//(* lento /2/*)
 #a #lea @a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a //
@@ -597,16 +539,16 @@ 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. *)
 
-img class="anchor" src="icons/tick.png" id="le_times"theorem le_times: ∀n1,n2,m1,m2:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. 
+theorem le_times: ∀n1,n2,m1,m2:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. 
 n1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2  → m1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m2 → n1a title="natural times" href="cic:/fakeuri.def(1)"*/am1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2a title="natural times" href="cic:/fakeuri.def(1)"*/am2.
 #n1 #n2 #m1 #m2 #len #lem @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (n1a title="natural times" href="cic:/fakeuri.def(1)"*/am2)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span/span/
 qed.
 
 (* interessante *)
-img class="anchor" src="icons/tick.png" id="lt_times_n"theorem lt_times_n: ∀n,m: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 than'" href="cic:/fakeuri.def(1)"</a n → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural times" href="cic:/fakeuri.def(1)"*/am.
+theorem lt_times_n: ∀n,m: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 than'" href="cic:/fakeuri.def(1)"</a n → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural times" href="cic:/fakeuri.def(1)"*/am.
 #n #m #H /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_times_to_le"theorem le_times_to_le: 
+theorem le_times_to_le: 
 ∀a,n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a → a a title="natural times" href="cic:/fakeuri.def(1)"*/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural times" href="cic:/fakeuri.def(1)"*/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 #a @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize
   [//
@@ -683,41 +625,41 @@ simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
 apply lt_plus.assumption.assumption.
 qed. *)
 
-img class="anchor" src="icons/tick.png" id="monotonic_lt_times_r"theorem monotonic_lt_times_r: 
+theorem monotonic_lt_times_r: 
   ∀c: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 than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/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 (λt.(ca title="natural times" href="cic:/fakeuri.def(1)"*/at)).
 #c #posc #n #m #ltnm
 (elim ltnm) normalize
-  [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(5)"monotonic_lt_plus_l/a/span/span/
+  [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a/span/span/ 
   |#a #_ #lt1 @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … lt1) //
   ]
 qed.
 
-img class="anchor" src="icons/tick.png" id="monotonic_lt_times_l"theorem monotonic_lt_times_l: 
+theorem monotonic_lt_times_l: 
   ∀c: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 than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/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 (λt.(ta title="natural times" href="cic:/fakeuri.def(1)"*/ac)).
-/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(9)"monotonic_lt_times_r/a/span/span/
+/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"monotonic_lt_times_r/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_to_le_to_lt_times"theorem lt_to_le_to_lt_times: 
+theorem lt_to_le_to_lt_times: 
 ∀n,m,p,q: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 → p a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a q → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq.
 #n #m #p #q #ltnm #lepq #posq
 @(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq))
   [@a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a //
-  |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"monotonic_lt_times_l/a //
+  |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(11)"monotonic_lt_times_l/a //
   ]
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_times"theorem lt_times:∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq.
-#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"lt_to_le_to_lt_times/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a, a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a/span/span/ 
+theorem lt_times:∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq.
+#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(12)"lt_to_le_to_lt_times/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a, a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a/span/span/ 
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_times_n_to_lt_l"theorem lt_times_n_to_lt_l: 
+theorem lt_times_n_to_lt_l: 
 ∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. pa title="natural times" href="cic:/fakeuri.def(1)"*/an a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a qa title="natural times" href="cic:/fakeuri.def(1)"*/an → p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q.
 #n #p #q #Hlt (elim (a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"decidable_lt/a p q)) //
 #nltpq @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ? ? (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a ? ? Hlt))
 applyS a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_lt_to_le.def(6)"not_lt_to_le/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_times_n_to_lt_r"theorem lt_times_n_to_lt_r: 
+theorem lt_times_n_to_lt_r: 
 ∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a na title="natural times" href="cic:/fakeuri.def(1)"*/aq → p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"lt_times_n_to_lt_l/a/span/span/ qed.
 
@@ -767,7 +709,7 @@ qed. *)
 
 (************************** minus ******************************)
 
-img class="anchor" src="icons/tick.png" id="minus"let rec minus n m ≝ 
+let rec minus n m ≝ 
  match n with 
  [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a
  | S p ⇒ 
@@ -777,22 +719,22 @@ qed. *)
         
 interpretation "natural minus" 'minus x y = (minus x y).
 
-img class="anchor" src="icons/tick.png" id="minus_S_S"theorem minus_S_S: ∀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 minus" href="cic:/fakeuri.def(1)"-/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/am.
+theorem minus_S_S: ∀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 minus" href="cic:/fakeuri.def(1)"-/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/am.
 // qed.
 
-img class="anchor" src="icons/tick.png" id="minus_O_n"theorem minus_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/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural minus" href="cic:/fakeuri.def(1)"-/an.
+theorem minus_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/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural minus" href="cic:/fakeuri.def(1)"-/an.
 #n (cases n) // qed.
 
-img class="anchor" src="icons/tick.png" id="minus_n_O"theorem minus_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ana title="natural minus" href="cic:/fakeuri.def(1)"-/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
+theorem minus_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ana title="natural minus" href="cic:/fakeuri.def(1)"-/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
 #n (cases n) // qed.
 
-img class="anchor" src="icons/tick.png" id="minus_n_n"theorem minus_n_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/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ana title="natural minus" href="cic:/fakeuri.def(1)"-/an.
+theorem minus_n_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/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ana title="natural minus" href="cic:/fakeuri.def(1)"-/an.
 #n (elim n) // qed.
 
-img class="anchor" src="icons/tick.png" id="minus_Sn_n"theorem minus_Sn_n: ∀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 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,2,0)"S/a n)a title="natural minus" href="cic:/fakeuri.def(1)"-/an.
+theorem minus_Sn_n: ∀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 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,2,0)"S/a n)a title="natural minus" href="cic:/fakeuri.def(1)"-/an.
 #n (elim n) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="minus_Sn_m"theorem minus_Sn_m: ∀m,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural minus" 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 minus" href="cic:/fakeuri.def(1)"-/am).
+theorem minus_Sn_m: ∀m,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural minus" 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 minus" href="cic:/fakeuri.def(1)"-/am).
 (* qualcosa da capire qui 
 #n #m #lenm nelim lenm napplyS refl_eq. *)
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a 
@@ -810,11 +752,11 @@ theorem not_eq_to_le_to_le_minus:
 napplyS (not_eq_to_le_to_lt n (S m) H H1)
 qed. *)
 
-img class="anchor" src="icons/tick.png" id="eq_minus_S_pred"theorem eq_minus_S_pred: ∀n,m. n a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a(n a title="natural minus" href="cic:/fakeuri.def(1)"-/am).
+theorem eq_minus_S_pred: ∀n,m. n a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a(n a title="natural minus" href="cic:/fakeuri.def(1)"-/am).
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize //
 qed.
 
-img class="anchor" src="icons/tick.png" id="plus_minus"theorem plus_minus:
+theorem plus_minus:
 ∀m,n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/ap a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/ap)a title="natural minus" href="cic:/fakeuri.def(1)"-/am.
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a 
   [//
@@ -823,27 +765,27 @@ qed.
   ]
 qed.
 
-img class="anchor" src="icons/tick.png" id="minus_plus_m_m"theorem minus_plus_m_m: ∀n,m: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)"+/am)a title="natural minus" href="cic:/fakeuri.def(1)"-/am.
+theorem minus_plus_m_m: ∀n,m: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)"+/am)a title="natural minus" href="cic:/fakeuri.def(1)"-/am.
 /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/plus_minus.def(5)"plus_minus/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="plus_minus_m_m"theorem plus_minus_m_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+theorem plus_minus_m_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
   m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/am.
 #n #m #lemn @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"plus_minus/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_plus_minus_m_m"theorem le_plus_minus_m_m: ∀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 (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/am.
+theorem le_plus_minus_m_m: ∀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 (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/am.
 #n (elim n) // #a #Hind #m (cases m) // normalize #n/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/  
 qed.
 
-img class="anchor" src="icons/tick.png" id="minus_to_plus"theorem minus_to_plus :∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+theorem minus_to_plus :∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
   m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a p → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap.
 #n #m #p #lemn #eqp (applyS a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a) //
 qed.
 
-img class="anchor" src="icons/tick.png" id="plus_to_minus"theorem plus_to_minus :∀n,m,p: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 ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a p.
+theorem plus_to_minus :∀n,m,p: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 ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a p.
 #n #m #p #eqp @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a (applyS (a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"minus_plus_m_m/a p m))
 qed.
 
-img class="anchor" src="icons/tick.png" id="minus_pred_pred"theorem minus_pred_pred : ∀n,m: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 than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → 
+theorem minus_pred_pred : ∀n,m: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 than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → 
 a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a m.
 #n #m #posn #posm @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a n posn) @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a m posm) //.
 qed.
@@ -900,7 +842,7 @@ qed.
 
 (* monotonicity and galois *)
 
-img class="anchor" src="icons/tick.png" id="monotonic_le_minus_l"theorem monotonic_le_minus_l: 
+theorem monotonic_le_minus_l: 
 ∀p,q,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → qa title="natural minus" href="cic:/fakeuri.def(1)"-/an a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural minus" href="cic:/fakeuri.def(1)"-/an.
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #p #q
   [#lePO @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a ? lePO) //
@@ -909,67 +851,72 @@ qed.
   ]
 qed.
 
-img class="anchor" src="icons/tick.png" id="le_minus_to_plus"theorem le_minus_to_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am.
+theorem le_minus_to_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am.
 #n #m #p #lep @a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a
-  [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ]
+  [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ]
 qed.
 
-img class="anchor" src="icons/tick.png" id="le_minus_to_plus_r"theorem le_minus_to_plus_r: ∀a,b,c. c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b.
-#a #b #c #Hlecb #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a … Hlecb) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_minus_to_plus.def(7)"le_minus_to_plus/a/span/span/
+theorem le_minus_to_plus_r: ∀a,b,c. c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b.
+#a #b #c #Hlecb #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a … Hlecb) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_minus_to_plus.def(10)"le_minus_to_plus/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="le_plus_to_minus"theorem le_plus_to_minus: ∀n,m,p. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p.
-#n #m #p #lep /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(5)"monotonic_le_minus_l/a/span/span/ qed.
+theorem le_plus_to_minus: ∀n,m,p. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p.
+#n #m #p #lep /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"monotonic_le_minus_l/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_plus_to_minus_r"theorem le_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c a title="natural minus" href="cic:/fakeuri.def(1)"-/ab.
+theorem le_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c a title="natural minus" href="cic:/fakeuri.def(1)"-/ab.
 #a #b #c #H @(a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"le_plus_to_le_r/a … b) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_minus_to_plus"theorem lt_minus_to_plus: ∀a,b,c. a a title="natural minus" href="cic:/fakeuri.def(1)"-/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a b.
+theorem lt_minus_to_plus: ∀a,b,c. a a title="natural minus" href="cic:/fakeuri.def(1)"-/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a b.
 #a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a 
-@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a …H)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"le_plus_to_minus_r/a/span/span/
+@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a …H)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"le_plus_to_minus_r/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_minus_to_plus_r"theorem lt_minus_to_plus_r: ∀a,b,c. a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b.
-#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a …))
+theorem lt_minus_to_plus_r: ∀a,b,c. a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b.
+#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a …))
 @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a //
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_plus_to_minus"theorem lt_plus_to_minus: ∀n,m,p. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p.
-#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a //
+theorem lt_plus_to_minus: ∀n,m,p. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p.
+#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a //
 qed.
 
-img class="anchor" src="icons/tick.png" id="lt_plus_to_minus_r"theorem lt_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural minus" href="cic:/fakeuri.def(1)"-/a b.
-#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"le_plus_to_minus_r/a //
+theorem lt_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural minus" href="cic:/fakeuri.def(1)"-/a b.
+#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"le_plus_to_minus_r/a //
 qed. 
 
-img class="anchor" src="icons/tick.png" id="monotonic_le_minus_r"theorem monotonic_le_minus_r: 
+theorem monotonic_le_minus_r: 
 ∀p,q,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural minus" href="cic:/fakeuri.def(1)"-/aq.
-#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a 
-@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a ? q)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/
+#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a 
+@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"le_plus_minus_m_m/a ? q)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="eq_minus_O"theorem eq_minus_O: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
+#p #q #n #H1 #H2
+@lt_plus_to_minus_r <plus_minus_m_m //
+qed.
+
+theorem eq_minus_O: ∀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 → na title="natural minus" 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,1,0)"O/a.
-#n #m #lenm @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_r.def(8)"monotonic_le_minus_r/a/span/span/
+#n #m #lenm @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_r.def(11)"monotonic_le_minus_r/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="distributive_times_minus"theorem distributive_times_minus: a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a ? a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/minus.fix(0,0,1)"minus/a.
+theorem distributive_times_minus: a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a ? a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/minus.fix(0,0,1)"minus/a.
 #a #b #c
 (cases (a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"decidable_lt/a b c)) #Hbc
- [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a // 
+ [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"eq_minus_O/a // 
   @a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/
  |@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a (applyS a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a) <a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"distributive_times_plus/a 
   @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a (applyS a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_lt_to_le.def(6)"not_lt_to_le/a/span/span/
 qed.
 
-img class="anchor" src="icons/tick.png" id="minus_plus"theorem minus_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/ama title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a(ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap).
+theorem minus_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/ama title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a(ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap).
 #n #m #p 
 cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a (ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap) n) #Hlt
   [@a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a @a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a
    @a href="cic:/matita/arithmetics/nat/minus_to_plus.def(8)"minus_to_plus/a //
   |cut (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap) [@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_n_Sn.def(1)"le_n_Sn/a …)) @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a //]
-   #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a, a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(5)"monotonic_le_minus_l/a/span/span/ 
+   #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"eq_minus_O/a, a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"monotonic_le_minus_l/a/span/span/ 
   ]
 qed.
 
@@ -979,7 +926,7 @@ theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
 >associative_plus <plus_minus_m_m //
 qed.  *)
 
-img class="anchor" src="icons/tick.png" id="minus_minus"theorem minus_minus: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. p a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n →
+theorem minus_minus: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. p a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n →
   pa title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural minus" href="cic:/fakeuri.def(1)"-/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural minus" href="cic:/fakeuri.def(1)"-/a(ma title="natural minus" href="cic:/fakeuri.def(1)"-/ap).
 #n #m #p #lepm #lemn
 @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a <a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a //
@@ -989,13 +936,13 @@ qed.
 (*********************** boolean arithmetics ********************) 
 include "basics/bool.ma".
 
-img class="anchor" src="icons/tick.png" id="eqb"let rec eqb n m ≝ 
+let rec eqb n m ≝ 
 match n with 
   [ O ⇒ match m with [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | S q ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] 
   | S p ⇒ match m with [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a | S q ⇒ eqb p q]
   ].
 
-img class="anchor" src="icons/tick.png" id="eqb_elim"theorem eqb_elim : ∀ n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
+theorem eqb_elim : ∀ n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
 (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am → (P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a)) → (n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → (P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a)) → (P (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m)). 
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a 
   [#n (cases n) normalize /span class="autotactic"3span class="autotrace" trace /span/span/ 
@@ -1004,23 +951,23 @@ match n with
   ] 
 qed.
 
-img class="anchor" src="icons/tick.png" id="eqb_n_n"theorem eqb_n_n: ∀n. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+theorem eqb_n_n: ∀n. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #n (elim n) normalize // qed. 
 
-img class="anchor" src="icons/tick.png" id="eqb_true_to_eq"theorem eqb_true_to_eq: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
+theorem eqb_true_to_eq: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
 #n #m @(a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"eqb_elim/a n m) // #_ #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="eqb_false_to_not_eq"theorem eqb_false_to_not_eq: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m.
+theorem eqb_false_to_not_eq: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m.
 #n #m @(a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"eqb_elim/a n 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.
 
-img class="anchor" src="icons/tick.png" id="eq_to_eqb_true"theorem eq_to_eqb_true: ∀n,m: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 m → a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+theorem eq_to_eqb_true: ∀n,m: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 m → a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 // qed.
 
-img class="anchor" src="icons/tick.png" id="not_eq_to_eqb_false"theorem not_eq_to_eqb_false: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+theorem not_eq_to_eqb_false: ∀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/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 #n #m #noteq @a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"eqb_elim/a// #Heq @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="leb"let rec leb n m ≝ 
+let rec leb n m ≝ 
 match n with 
     [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a
     | (S p) ⇒
@@ -1028,7 +975,7 @@ match n with
         [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
 	      | (S q) ⇒ leb p q]].
 
-img class="anchor" src="icons/tick.png" id="leb_elim"theorem leb_elim: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ∀P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop. 
+theorem leb_elim: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ∀P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop. 
 (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → P (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m).
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize
   [/span class="autotactic"2span class="autotrace" trace /span/span/
@@ -1038,20 +985,20 @@ match n with
   ]
 qed.
 
-img class="anchor" src="icons/tick.png" id="leb_true_to_le"theorem leb_true_to_le:∀n,m.a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+theorem leb_true_to_le:∀n,m.a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 #n #m @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a // #_ #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="leb_false_to_not_le"theorem leb_false_to_not_le:∀n,m.
+theorem leb_false_to_not_le:∀n,m.
   a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m.
 #n #m @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a // #_ #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_to_leb_true"theorem le_to_leb_true: ∀n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+theorem le_to_leb_true: ∀n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #n #m @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a // #H #H1 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="not_le_to_leb_false"theorem not_le_to_leb_false: ∀n,m. n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
+theorem not_le_to_leb_false: ∀n,m. n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 #n #m @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a // #H #H1 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="lt_to_leb_false"theorem lt_to_leb_false: ∀n,m. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
+theorem lt_to_leb_false: ∀n,m. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a, a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"not_le_to_leb_false/a/span/span/ qed.
 
 (* serve anche ltb? 
@@ -1080,41 +1027,40 @@ theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
 qed. *)
 
 (* min e max *)
-img class="anchor" src="icons/tick.png" id="min"definition min: 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.ind(1,0,0)"nat/a ≝
+definition min: 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.ind(1,0,0)"nat/a ≝
 λn.λm. if (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m) then n else m.
 
-img class="anchor" src="icons/tick.png" id="max"definition max: 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.ind(1,0,0)"nat/a ≝
+definition max: 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.ind(1,0,0)"nat/a ≝
 λn.λm. if (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m) then m else n.
 
-img class="anchor" src="icons/tick.png" id="commutative_min"lemma commutative_min: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/min.def(2)"min/a.
+lemma commutative_min: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/min.def(2)"min/a.
 #n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a 
   [@a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"le_to_le_to_eq/a/span/span/
   |#notle >(a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a …) // @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/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/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/
   ] qed.
 
-img class="anchor" src="icons/tick.png" id="le_minr"lemma le_minr: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+lemma le_minr: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 #i #n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed. 
 
-img class="anchor" src="icons/tick.png" id="le_minl"lemma le_minl: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+lemma le_minl: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_minr.def(7)"le_minr/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="to_min"lemma to_min: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m.
+lemma to_min: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m.
 #i #n #m #lein #leim normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) 
 normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="commutative_max"lemma commutative_max: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/max.def(2)"max/a.
+lemma commutative_max: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/max.def(2)"max/a.
 #n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a 
   [@a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"le_to_le_to_eq/a/span/span/
   |#notle >(a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a …) // @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/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/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/
   ] qed.
 
-img class="anchor" src="icons/tick.png" id="le_maxl"lemma le_maxl: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
+lemma le_maxl: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
 #i #n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed. 
 
-img class="anchor" src="icons/tick.png" id="le_maxr"lemma le_maxr: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
+lemma le_maxr: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="to_max"lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
+lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
 #i #n #m #leni #lemi normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) 
-normalize // qed.
-
+normalize // qed.
\ No newline at end of file