From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 Apr 2013 16:09:28 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1177
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=569ba7fe357918e3e83c3fe2d5a41070834c5b67;p=helm.git

commit by user andrea
---

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index 638b7ac91..ee4362b71 100644
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -14,10 +14,8 @@ definition eqvar ≝ λv1,v2.
 definition update : state → Var → nat → state ≝ λs,v,a,v1. 
   if eqvar v1 v then a else s v1.
 
-
 (* Semantics of Arithmetic expressions *)
-pre class="smallmargin" style="display: inline;"
-let rec evalA a s ≝
+pre class="smallmargin" style="display: inline;"let rec evalA a s ≝
   match a with 
   [ Const n => n
   | Aid v => s v
@@ -30,7 +28,7 @@ let rec evalA a s ≝
  .
 
 example exA1: evalA ((Const 2)+(Const 3)*(Aid (Id 2))) (λx.span style="text-decoration: underline;"1/span) = span style="text-decoration: underline;"5/span.
-normalize // qed. 
+normalize // qed 
 
 let rec evalB b s ≝
   match b with
diff --git a/weblib/arithmetics/bigops.ma b/weblib/arithmetics/bigops.ma
index 03db53f7d..0c10b02bb 100644
--- a/weblib/arithmetics/bigops.ma
+++ b/weblib/arithmetics/bigops.ma
@@ -12,36 +12,28 @@
 include "basics/types.ma".
 include "arithmetics/div_and_mod.ma".
 
-definition sameF_upto: nat → ∀A.relation(nat→A)  ≝
-λk.λA.λf,g.∀i. i < k → f i = g i.
+img class="anchor" src="icons/tick.png" id="sameF_upto"definition sameF_upto: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → ∀A.a href="cic:/matita/basics/relations/relation.def(1)"relation/a(a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→A)  ≝
+λk.λA.λf,g.∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a k → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g i.
      
-definition sameF_p: nat → (nat → bool) →∀A.relation(nat→A)  ≝
-λk,p,A,f,g.∀i. i < k → p i = true → f i = g i.
+img class="anchor" src="icons/tick.png" id="sameF_p"definition sameF_p: 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/basics/bool/bool.ind(1,0,0)"bool/a) →∀A.a href="cic:/matita/basics/relations/relation.def(1)"relation/a(a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→A)  ≝
+λk,p,A,f,g.∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a k → p i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g i.
 
-lemma sameF_upto_le: ∀A,f,g,n,m. 
- n ≤m → sameF_upto m A f g → sameF_upto n A f g.
-#A #f #g #n #m #lenm #samef #i #ltin @samef /2/
+img class="anchor" src="icons/tick.png" id="sameF_upto_le"lemma sameF_upto_le: ∀A,f,g,n,m. 
+ n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am → a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"sameF_upto/a m A f g → a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"sameF_upto/a n A f g.
+#A #f #g #n #m #lenm #samef #i #ltin @samef /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a/span/span/
 qed.
 
-lemma sameF_p_le: ∀A,p,f,g,n,m. 
- n ≤m → sameF_p m p A f g → sameF_p n p A f g.
-#A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /2/
+img class="anchor" src="icons/tick.png" id="sameF_p_le"lemma sameF_p_le: ∀A,p,f,g,n,m. 
+ n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am → a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"sameF_p/a m p A f g → a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"sameF_p/a n p A f g.
+#A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a/span/span/
 qed.
 
-(*
-definition sumF ≝ λA.λf,g:nat → A.λn,i.
-if_then_else ? (leb n i) (g (i-n)) (f i). 
-
-lemma sumF_unfold: ∀A,f,g,n,i. 
-sumF A f g n i = if_then_else ? (leb n i) (g (i-n)) (f i). 
-// qed. *)
-
-definition prodF ≝
- λA,B.λf:nat→A.λg:nat→B.λm,x.〈 f(div x m), g(mod x m) 〉.
+img class="anchor" src="icons/tick.png" id="prodF"definition prodF ≝
+ λA,B.λf:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→A.λg:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.λm,x.〈 f(a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a x m), g(a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a x m) a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a.
 
 (* bigop *)
-let rec bigop (n:nat) (p:nat → bool) (B:Type[0])
-   (nil: B) (op: B → B → B)  (f: nat → B) ≝
+img class="anchor" src="icons/tick.png" id="bigop"let rec bigop (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 → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (B:Type[0])
+   (nil: B) (op: B → B → B)  (f: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → B) ≝
   match n with
    [ O ⇒ nil
    | S k ⇒ 
@@ -64,12 +56,12 @@ notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
   with precedence 80
 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-  
+
 notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
   with precedence 80
 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.  
- 
+
 (* notation "\big  [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
   with precedence 80
 for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}.
@@ -77,947 +69,350 @@ for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))
  
 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
    
-lemma bigop_Strue: ∀k,p,B,nil,op.∀f:nat→B. p k = true →
-  \big[op,nil]_{i < S k | p i}(f i) =
-    op (f k) (\big[op,nil]_{i < k | p i}(f i)).
+img class="anchor" src="icons/tick.png" id="bigop_Strue"lemma bigop_Strue: ∀k,p,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. p k a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
+  \big[op,nil]_{i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    op (f k) (\big[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)).
 #k #p #B #nil #op #f #H normalize >H // qed.
 
-lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:nat→B. p k = false →
-  \big[op,nil]_{ i < S k | p i}(f i) =
-    \big[op,nil]_{i < k | p i}(f i).
+img class="anchor" src="icons/tick.png" id="bigop_Sfalse"lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. p k a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a →
+  \big[op,nil]_{ i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    \big[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
 #k #p #B #nil #op #f #H normalize >H // qed. 
  
-lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:nat→B. 
-  sameF_upto k bool p1 p2 → sameF_p k p1 B f g →
-  \big[op,nil]_{i < k | p1 i}(f i) = 
-    \big[op,nil]_{i < k | p2 i}(g i).
+img class="anchor" src="icons/tick.png" id="same_bigop"lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. 
+  a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"sameF_upto/a k a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a p1 p2 → a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"sameF_p/a k p1 B f g →
+  \big[op,nil]_{i < k | p1 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    \big[op,nil]_{i < k | p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(g i).
 #k #p1 #p2 #B #nil #op #f #g (elim k) // 
-#n #Hind #samep #samef normalize >Hind /2/
-<(samep … (le_n …)) cases(true_or_false (p1 n)) #H1 >H1 
-normalize // <(samef … (le_n …) H1) // 
+#n #Hind #samep #samef normalize >Hind 
+  [|@(a href="cic:/matita/arithmetics/bigops/sameF_p_le.def(5)"sameF_p_le/a … samef) // |@(a href="cic:/matita/arithmetics/bigops/sameF_upto_le.def(5)"sameF_upto_le/a … samep) //]
+<(samep … (a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a …)) cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p1 n)) #H1 >H1 
+normalize // <(samef … (a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a …) H1) // 
 qed.
 
-theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k → 
-\big[op,nil]_{i < n | p i}(f i)
-  = \big[op,nil]_{i < k | if_then_else ? (leb n i) false (p i)}(f i).
+img class="anchor" src="icons/tick.png" id="pad_bigop"theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a k → 
+\big[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)
+  a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < k | font class="Apple-style-span" color="#FF0000"if/font (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n i) then a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a else p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
 #k #n #p #B #nil #op #f #lenk (elim lenk) 
-  [@same_bigop #i #lti // >(not_le_to_leb_false …) /2/
-  |#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) // 
+  [@a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #lti // >(a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"not_le_to_leb_false/a …) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a/span/span/
+  |#j #leup #Hind >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a >(a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a … leup) // 
   ] qed.
 
-record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+img class="anchor" src="icons/tick.png" id="pad_bigop1"theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a k → 
+  (∀i. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a k → p i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) →
+  \big[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) 
+    a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
+#k #n #p #B #nil #op #f #lenk (elim lenk) 
+  [#_ @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #lti // 
+  |#j #leup #Hind #Hfalse >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a 
+    [@Hind #i #leni #ltij @Hfalse // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //  
+    |@Hfalse // 
+    ] 
+  ] 
+qed.
+
+img class="anchor" src="icons/tick.png" id="bigop_false"theorem bigop_false: ∀n,B,nil,op.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
+  \big[op,nil]_{i < n | a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a nil.  
+#n #B #nil #op #f elim n // #n1 #Hind 
+>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // 
+qed.
+
+img class="anchor" src="icons/tick.png" id="Aop"record Aop (A:Type[0]) (nil:A) : Type[0] ≝
   {op :2> A → A → A; 
-   nill:∀a. op nil a = a; 
-   nilr:∀a. op a nil = a;
-   assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+   nill:∀a. op nil a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; 
+   nilr:∀a. op a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a;
+   assoc: ∀a,b,c.op a (op b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a op (op a b) c
   }.
 
-theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B.
-op (\big[op,nil]_{i<k1|p1 i}(f i)) \big[op,nil]_{i<k2|p2 i}(g i) =
-      \big[op,nil]_{i<k1+k2|if_then_else ? (leb k2 i) (p1 (i-k2)) (p2 i)}
-        (if_then_else ? (leb k2 i) (f (i-k2)) (g i)).
+img class="anchor" src="icons/tick.png" id="pad_bigop_nil"theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a k → 
+  (∀i. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a k → p i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a nil) →
+  \big[op,nil]_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) 
+    a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < k | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
+#k #n #p #B #nil #op #f #lenk (elim lenk) 
+  [#_ @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #lti // 
+  |#j #leup #Hind #Hfalse cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p j)) #Hpj
+    [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // 
+     cut (f j a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a nil) 
+      [cases (Hfalse j leup (a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a … )) // >Hpj #H destruct (H)] #Hfj
+     >Hfj >a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"nill/a @Hind #i #leni #ltij
+     cases (Hfalse i leni (a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a … ltij)) /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/
+    |>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // @Hind #i #leni #ltij
+     cases (Hfalse i leni (a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a … ltij)) /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/
+    ]  
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="bigop_sum"theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
+op (\big[op,nil]_{i<k1|p1 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)) \big[op,nil]_{i<k2|p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(g i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+      \big[op,nil]_{i<k1a title="natural plus" href="cic:/fakeuri.def(1)"+/ak2|font class="Apple-style-span" color="#FF0000" if /fonta href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a k2 i then p1 (ia title="natural minus" href="cic:/fakeuri.def(1)"-/ak2) else p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a
+        (if a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a k2 i then f (ia title="natural minus" href="cic:/fakeuri.def(1)"-/ak2) else g i).
 #k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
-  [normalize >nill @same_bigop #i #lti 
-   >(lt_to_leb_false … lti) normalize /2/
-  |#i #Hind normalize <minus_plus_m_m (cases (p1 i)) 
-   >(le_to_leb_true … (le_plus_n …)) normalize <Hind //
-   <assoc //
+  [normalize >a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"nill/a @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #lti 
+   >(a href="cic:/matita/arithmetics/nat/lt_to_leb_false.def(8)"lt_to_leb_false/a … lti) normalize /span class="autotactic"2span class="autotrace" trace /span/span/
+  |#i #Hind normalize <a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"minus_plus_m_m/a (cases (p1 i)) 
+   >(a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a … (a href="cic:/matita/arithmetics/nat/le_plus_n.def(7)"le_plus_n/a …)) normalize <Hind //
+   <a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"assoc/a //
   ]
 qed.
 
-lemma plus_minus1: ∀a,b,c. c ≤ b → a + (b -c) = a + b -c.
-#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c)
->associative_plus <plus_minus_m_m //
+img class="anchor" src="icons/tick.png" id="plus_minus1"lemma plus_minus1: ∀a,b,c. c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a (b a title="natural minus" href="cic:/fakeuri.def(1)"-/ac) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/ac.
+#a #b #c #lecb @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/commutative_plus.def(5)"commutative_plus/a c)
+>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 //
+qed.
+
+img class="anchor" src="icons/tick.png" id="bigop_I"theorem bigop_I: ∀n,p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
+\big[op,nil]_{i∈[a title="natural number" href="cic:/fakeuri.def(1)"0/a,n[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < n|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i). 
+#n #p #B #nil #op #f <a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"minus_n_O/a @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a //
 qed.
 
-theorem bigop_I: ∀n,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
-\big[op,nil]_{i∈[0,n[ |p i}(f i) = \big[op,nil]_{i < n|p i}(f i). 
-#n #p #B #nil #op #f <minus_n_O @same_bigop //
+img class="anchor" src="icons/tick.png" id="bigop_I_gen"theorem bigop_I_gen: ∀a,b,p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/ab →
+\big[op,nil]_{i∈[a,b[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i < b|a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a a i a title="boolean and" href="cic:/fakeuri.def(1)"∧/a p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i). 
+#a #b elim b // -b #b #Hind #p #B #nil #op #f #lea
+cut (∀a,b. a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a 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 (b a title="natural minus" href="cic:/fakeuri.def(1)"-/aa)) 
+  [#a #b cases a // #a1 #lta1 normalize >a href="cic:/matita/arithmetics/nat/eq_minus_S_pred.def(4)"eq_minus_S_pred/a >a href="cic:/matita/arithmetics/nat/S_pred.def(3)"S_pred/a 
+   /2 by a href="cic:/matita/arithmetics/nat/lt_plus_to_minus_r.def(11)"lt_plus_to_minus_r/a/] #Hcut
+cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lea) #Ha
+  [cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p b)) #Hcase
+    [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a [2: >Hcase >(a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a a b) // @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @Ha]
+     >(Hcut … (a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a … Ha))
+     >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a 
+      [@a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a 
+        [@a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a <a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a [//|@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a //] @Hind 
+        |@Hind @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/plus_minus_m_m.def(7)"plus_minus_m_m/a // @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a //
+      ]
+   |>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a [2: >Hcase cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a a b)//]
+     >(Hcut … (a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a … Ha)) >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a
+      [@Hind @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/plus_minus_m_m.def(7)"plus_minus_m_m/a // @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a //]
+    ]
+  |<Ha <a href="cic:/matita/arithmetics/nat/minus_n_n.def(4)"minus_n_n/a whd in ⊢ (??%?); <(a href="cic:/matita/arithmetics/bigops/bigop_false.def(4)"bigop_false/a a B nil op f) in ⊢ (??%?);
+   @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a // #i #ltia >(a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"not_le_to_leb_false/a a i) // @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a //
+  ]
 qed.
           
-theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
-a ≤ b → b ≤ c →
-\big[op,nil]_{i∈[a,c[ |p i}(f i) = 
-  op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i)) 
-      \big[op,nil]_{i ∈ [a,b[ |p i}(f i).
+img class="anchor" src="icons/tick.png" id="bigop_sumI"theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
+a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c →
+\big[op,nil]_{i∈[a,c[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  op (\big[op,nil]_{i ∈ [b,c[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)) 
+      \big[op,nil]_{i ∈ [a,b[ |p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i).
 #a #b # c #p #B #nil #op #f #leab #lebc 
->(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?) /2/
->minus_plus >(commutative_plus a) <plus_minus_m_m //
->bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
-  [#i #lei >plus_minus // <plus_minus1 
-     [@eq_f @sym_eq @plus_to_minus /2/ | /2/]] 
-#H @same_bigop #i #ltic @leb_elim normalize // #lei <H //
+>(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a (ca title="natural minus" href="cic:/fakeuri.def(1)"-/aa) (ba title="natural minus" href="cic:/fakeuri.def(1)"-/aa)) in ⊢ (??%?); /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/
+>a href="cic:/matita/arithmetics/nat/minus_plus.def(13)"minus_plus/a >(a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a a) <a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a //
+>a href="cic:/matita/arithmetics/bigops/bigop_sum.def(9)"bigop_sum/a (cut (∀i. b a title="natural minus" href="cic:/fakeuri.def(1)"-/aa a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → ia title="natural plus" href="cic:/fakeuri.def(1)"+/aa a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ia title="natural minus" href="cic:/fakeuri.def(1)"-/a(ba title="natural minus" href="cic:/fakeuri.def(1)"-/aa)a title="natural plus" href="cic:/fakeuri.def(1)"+/ab))
+  [#i #lei >a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"plus_minus/a // <a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"plus_minus1/a 
+     [@a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @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 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"plus_minus1/a/span/span/ | /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/]] 
+#H @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a #i #ltic @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize // #lei <H //
 qed.   
 
-theorem bigop_a: ∀a,b,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤ b →
-\big[op,nil]_{i∈[a,S b[ }(f i) = 
-  op (\big[op,nil]_{i ∈ [a,b[ }(f (S i))) (f a).
+img class="anchor" src="icons/tick.png" id="bigop_a"theorem bigop_a: ∀a,b,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B. a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b →
+\big[op,nil]_{i∈[a,a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b[ a title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  op (\big[op,nil]_{i ∈ [a,b[ a title="bigop" href="cic:/fakeuri.def(1)"}/a(f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i))) (f a).
 #a #b #B #nil #op #f #leab 
->(bigop_sumI a (S a) (S b)) [|@le_S_S //|//] @eq_f2 
-  [@same_bigop // |<minus_Sn_n normalize @nilr]
+>(a href="cic:/matita/arithmetics/bigops/bigop_sumI.def(14)"bigop_sumI/a a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a) (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b)) [|@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a //|//] @a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a 
+  [@a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a // |<a href="cic:/matita/arithmetics/nat/minus_Sn_n.def(4)"minus_Sn_n/a normalize @a href="cic:/matita/arithmetics/bigops/nilr.fix(0,2,2)"nilr/a]
 qed.
   
-theorem bigop_0: ∀n,B.∀nil.∀op:Aop B nil.∀f:nat→B.
-\big[op,nil]_{i < S n}(f i) = 
-  op (\big[op,nil]_{i < n}(f (S i))) (f 0).
+img class="anchor" src="icons/tick.png" id="bigop_0"theorem bigop_0: ∀n,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→B.
+\big[op,nil]_{i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  op (\big[op,nil]_{i < na title="bigop" href="cic:/fakeuri.def(1)"}/a(f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i))) (f a title="natural number" href="cic:/fakeuri.def(1)"0/a).
 #n #B #nil #op #f 
-<bigop_I >bigop_a [|//] @eq_f2 [|//] <minus_n_O 
-@same_bigop //
+<a href="cic:/matita/arithmetics/bigops/bigop_I.def(7)"bigop_I/a >a href="cic:/matita/arithmetics/bigops/bigop_a.def(15)"bigop_a/a [|//] @a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a [|//] <a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"minus_n_O/a 
+@a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a //
 qed.    
 
-theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat → B.
-\big[op,nil]_{x<k1|p1 x}(\big[op,nil]_{i<k2|p2 x i}(f x i)) =
-  \big[op,nil]_{i<k1*k2|andb (p1 (div i k2)) (p2 (div i k2) (i \mod k2))}
-     (f (div i k2) (i \mod k2)).
+img class="anchor" src="icons/tick.png" id="bigop_prod"theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a B nil.∀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 → B.
+\big[op,nil]_{x<k1|p1 xa title="bigop" href="cic:/fakeuri.def(1)"}/a(\big[op,nil]_{i<k2|p2 x ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f x i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+  \big[op,nil]_{i<k1a title="natural times" href="cic:/fakeuri.def(1)"*/ak2|a href="cic:/matita/basics/bool/andb.def(1)"andb/a (p1 (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a i k2)) (p2 (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a i k2) (i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a k2))a title="bigop" href="cic:/fakeuri.def(1)"}/a
+     (f (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a i k2) (i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a k2)).
 #k1 #k2 #p1 #p2 #B #nil #op #f (elim k1) //
-#n #Hind cases(true_or_false (p1 n)) #Hp1
-  [>bigop_Strue // >Hind >bigop_sum @same_bigop
-   #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
-   #eqi [|#H] (>eqi in ⊢ (???%))
-     >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/
-  |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
-   #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
-   #eqi >eqi in ⊢ (???%) >div_plus_times /2/ 
+#n #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p1 n)) #Hp1
+  [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >Hind >a href="cic:/matita/arithmetics/bigops/bigop_sum.def(9)"bigop_sum/a @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a
+   #i #lti @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a // #lei cut (i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/ak2a title="natural plus" href="cic:/fakeuri.def(1)"+/a(ia title="natural minus" href="cic:/fakeuri.def(1)"-/ana title="natural times" href="cic:/fakeuri.def(1)"*/ak2)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"plus_minus1/a/span/span/
+   #eqi [|#H] >eqi in ⊢ (???%);
+     >a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"div_plus_times/a /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/ >Hp1 >(a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"mod_plus_times/a …) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"lt_plus_to_lt_l/a/span/span/
+  |>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // >Hind >(a href="cic:/matita/arithmetics/bigops/pad_bigop.def(8)"pad_bigop/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="natural times" href="cic:/fakeuri.def(1)"*/ak2)) // @a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a
+   #i #lti @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a // #lei cut (i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/ak2a title="natural plus" href="cic:/fakeuri.def(1)"+/a(ia title="natural minus" href="cic:/fakeuri.def(1)"-/ana title="natural times" href="cic:/fakeuri.def(1)"*/ak2)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"plus_minus1/a/span/span/
+   #eqi >eqi in ⊢ (???%); >a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"div_plus_times/a [ >Hp1 %| /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_minus_l.def(12)"monotonic_lt_minus_l/a/span/span/]
   ]
 qed.
 
-record ACop (A:Type[0]) (nil:A) : Type[0] ≝
-  {aop :> Aop A nil; 
-   comm: ∀a,b.aop a b = aop b a
+img class="anchor" src="icons/tick.png" id="ACop"record ACop (A:Type[0]) (nil:A) : Type[0] ≝
+  {aop :> a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"Aop/a A nil; 
+   comm: ∀a,b.aop a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a aop b a
   }.
  
-lemma bigop_op: ∀k,p,B.∀nil.∀op:ACop B nil.∀f,g: nat → B.
-op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p i}(g i)) =
-  \big[op,nil]_{i<k|p i}(op (f i) (g i)).
-#k #p #B #nil #op #f #g (elim k) [normalize @nill]
--k #k #Hind (cases (true_or_false (p k))) #H
-  [>bigop_Strue // >bigop_Strue // >bigop_Strue //
-   <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?) 
-   <assoc @eq_f @Hind
-  |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
+img class="anchor" src="icons/tick.png" id="bigop_op"lemma bigop_op: ∀k,p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a B nil.∀f,g: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → B.
+op (\big[op,nil]_{i<k|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i)) (\big[op,nil]_{i<k|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(g i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+  \big[op,nil]_{i<k|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(op (f i) (g i)).
+#k #p #B #nil #op #f #g (elim k) [normalize @a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"nill/a]
+-k #k #Hind (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p k))) #H
+  [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a //
+   normalize <a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"assoc/a <a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"assoc/a in ⊢ (???%); @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a >a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"assoc/a 
+   >a href="cic:/matita/arithmetics/bigops/comm.fix(0,2,3)"comm/a in ⊢ (??(????%?)?); <a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"assoc/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @Hind
+  |>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a //
   ]
 qed.
 
-lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
-  i < n → p i = true →
-  \big[op,nil]_{x<n|p x}(f x)=
-    op (f i) (\big[op,nil]_{x<n|andb(notb(eqb i x))(p x)}(f x)).
+img class="anchor" src="icons/tick.png" id="bigop_diff"lemma bigop_diff: ∀p,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a B nil.∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → B.∀i,n.
+  i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → p i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
+  \big[op,nil]_{x<n|p xa title="bigop" href="cic:/fakeuri.def(1)"}/a(f x)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    op (f i) (\big[op,nil]_{x<n|a href="cic:/matita/basics/bool/andb.def(1)"andb/a(a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a i x))(p x)a title="bigop" href="cic:/fakeuri.def(1)"}/a(f x)).
 #p #B #nil #op #f #i #n (elim n) 
-  [#ltO @False_ind /2/
-  |#n #Hind #lein #pi cases (le_to_or_lt_eq … (le_S_S_to_le …lein)) #Hi
-    [cut (andb(notb(eqb i n))(p n) = (p n))
-      [>(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut
-     cases (true_or_false (p n)) #pn 
-      [>bigop_Strue // >bigop_Strue //
-       >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
-      |>bigop_Sfalse // >bigop_Sfalse // >Hind //  
+  [#ltO @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/
+  |#n #Hind #lein #pi cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … (a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a …lein)) #Hi
+    [cut (a href="cic:/matita/basics/bool/andb.def(1)"andb/a(a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a i n))(p n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (p n))
+      [>(a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"not_eq_to_eqb_false/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a … Hi)) //] #Hcut
+     cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p n)) #pn 
+      [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a //
+       normalize >a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"assoc/a >(a href="cic:/matita/arithmetics/bigops/comm.fix(0,2,3)"comm/a ?? op (f i) (f n)) <a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"assoc/a >Hind //
+      |>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // >Hind //  
       ]
-    |<Hi >bigop_Strue // @eq_f >bigop_Sfalse  
-       [@same_bigop // #k #ltki >not_eq_to_eqb_false /2/
-       |>eq_to_eqb_true // 
+    |<Hi >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a  
+       [@a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"same_bigop/a // #k #ltki >a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"not_eq_to_eqb_false/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/
+       |>a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"eq_to_eqb_true/a // 
        ]
      ]
    ]
 qed.
 
 (* range *)
-record range (A:Type[0]): Type[0] ≝
-  {enum:nat→A; upto:nat; filter:nat→bool}.
+img class="anchor" src="icons/tick.png" id="range"record range (A:Type[0]): Type[0] ≝
+  {enum:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→A; upto:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a; filter:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a}.
   
-definition sub_hk: (nat→nat)→(nat→nat)→∀A:Type[0].relation (range A) ≝
-λh,k,A,I,J.∀i.i<(upto A I) → (filter A I i)=true → 
-  (h i < upto A J
-  ∧ filter A J (h i) = true
-  ∧ k (h i) = i).
-
-definition iso: ∀A:Type[0].relation (range A) ≝
-  λA,I,J.∃h,k. 
-    (∀i. i < (upto A I) → (filter A I i) = true → 
-       enum A I i = enum A J (h i)) ∧
-    sub_hk h k A I J ∧ sub_hk k h A J I.
+img class="anchor" src="icons/tick.png" id="sub_hk"definition sub_hk: (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→a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a)→∀A:Type[0].a href="cic:/matita/basics/relations/relation.def(1)"relation/a (a href="cic:/matita/arithmetics/bigops/range.ind(1,0,1)"range/a A) ≝
+λh,k,A,I,J.∀i.ia title="natural 'less than'" href="cic:/fakeuri.def(1)"</a(a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"upto/a A I) → (a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"filter/a A I i)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+  (h i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"upto/a A J
+  a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"filter/a A J (h i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a
+  a title="logical and" href="cic:/fakeuri.def(1)"∧/a k (h i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i).
+
+img class="anchor" src="icons/tick.png" id="iso"definition iso: ∀A:Type[0].a href="cic:/matita/basics/relations/relation.def(1)"relation/a (a href="cic:/matita/arithmetics/bigops/range.ind(1,0,1)"range/a A) ≝
+  λA,I,J.a title="exists" href="cic:/fakeuri.def(1)"∃/ah,ka title="exists" href="cic:/fakeuri.def(1)"./a 
+    (∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a (a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"upto/a A I) → (a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"filter/a A I i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+       a href="cic:/matita/arithmetics/bigops/enum.fix(0,1,1)"enum/a A I i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/bigops/enum.fix(0,1,1)"enum/a A J (h i)) a title="logical and" href="cic:/fakeuri.def(1)"∧/a
+    a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"sub_hk/a h k A I J a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"sub_hk/a k h A J I.
   
-lemma sub_hkO: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A I J.
-#h #k #A #I #J #up0 #i #lti >up0 @False_ind /2/
+img class="anchor" src="icons/tick.png" id="sub_hkO"lemma sub_hkO: ∀h,k,A,I,J. a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"upto/a A I a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"0/a → a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"sub_hk/a h k A I J.
+#h #k #A #I #J #up0 #i #lti >up0 @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.
 
-lemma sub0_to_false: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A J I → 
-  ∀i. i < upto A J → filter A J i = false.
-#h #k #A #I #J #up0 #sub #i #lti cases(true_or_false (filter A J i)) //
-#ptrue (cases (sub i lti ptrue)) * #hi @False_ind /2/ 
+img class="anchor" src="icons/tick.png" id="sub0_to_false"lemma sub0_to_false: ∀h,k,A,I,J. a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"upto/a A I a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"0/a → a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"sub_hk/a h k A J I → 
+  ∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"upto/a A J → a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"filter/a A J i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
+#h #k #A #I #J #up0 #sub #i #lti cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"filter/a A J i)) //
+#ptrue (cases (sub i lti ptrue)) * #hi @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.
 
-lemma sub_lt: ∀A,e,p,n,m. n ≤ m → 
-  sub_hk (λx.x) (λx.x) A (mk_range A e n p) (mk_range A e m p).
-#A #e #f #n #m #lenm #i #lti #fi % // % /2/
+img class="anchor" src="icons/tick.png" id="sub_lt"lemma sub_lt: ∀A,e,p,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → 
+  a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"sub_hk/a (λx.x) (λx.x) A (a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"mk_range/a A e n p) (a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"mk_range/a A e m p).
+#A #e #f #n #m #lenm #i #lti #fi % // % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a/span/span/
 qed. 
 
-theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K. 
-  sub_hk h1 k1 A I J → sub_hk h2 k2 A J K → 
-    sub_hk (λx.h2(h1 x)) (λx.k1(k2 x)) A I K.
+img class="anchor" src="icons/tick.png" id="transitive_sub"theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K. 
+  a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"sub_hk/a h1 k1 A I J → a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"sub_hk/a h2 k2 A J K → 
+    a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"sub_hk/a (λx.h2(h1 x)) (λx.k1(k2 x)) A I K.
 #h1 #k1 #h2 #k2 #A #I #J #K #sub1 #sub2 #i #lti #fi 
 cases(sub1 i lti fi) * #lth1i #fh1i #ei 
 cases(sub2 (h1 i) lth1i fh1i) * #H1 #H2 #H3 % // % // 
 qed. 
 
-theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
-  iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
-  \big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
+img class="anchor" src="icons/tick.png" id="bigop_iso"theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a B nil.∀f1,f2.
+  a href="cic:/matita/arithmetics/bigops/iso.def(3)"iso/a B (a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"mk_range/a B f1 n1 p1) (a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"mk_range/a B f2 n2 p2) →
+  \big[op,nil]_{i<n1|p1 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f1 i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a \big[op,nil]_{i<n2|p2 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f2 i).
 #n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
-@(le_gen ? n1) #i (generalize in match p2) (elim i) 
+@(a href="cic:/matita/arithmetics/nat/le_gen.def(1)"le_gen/a ? n1) #i generalize in match p2; (elim i) 
   [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
-   >bigop_Sfalse 
-    [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
-    |@(sub0_to_false … sub2) //
+   >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a 
+    [@(Hind ? (a href="cic:/matita/arithmetics/nat/le_O_n.def(2)"le_O_n/a ?)) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/bigops/sub_hkO.def(4)"sub_hkO/a/span/span/ | @(a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"transitive_sub/a … (a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"sub_lt/a …) sub2) //]
+    |@(a href="cic:/matita/arithmetics/bigops/sub0_to_false.def(4)"sub0_to_false/a … sub2) //
     ]
-  |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n ≤n1)) [/2/] #len
-   cases(true_or_false (p1 n)) #p1n
-    [>bigop_Strue // (cases (sub1 n (le_n …) p1n)) * #hn #p2hn #eqn
-     >(bigop_diff … (h n) n2) // >same // 
-     @eq_f @(Hind ? len)
-      [#i #ltin #p1i (cases (sub1 i (le_S … ltin) p1i)) * 
-       #h1i #p2h1i #eqi % // % // >not_eq_to_eqb_false normalize // 
-       @(not_to_not ??? (lt_to_not_eq ? ? ltin)) // 
-      |#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) * 
+  |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/an1)) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/] #len
+   cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p1 n)) #p1n
+    [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // (cases (sub1 n (a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a …) p1n)) * #hn #p2hn #eqn
+     >(a href="cic:/matita/arithmetics/bigops/bigop_diff.def(8)"bigop_diff/a … (h n) n2) // >same // 
+     @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(Hind ? len)
+      [#i #ltin #p1i (cases (sub1 i (a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a … ltin) p1i)) * 
+       #h1i #p2h1i #eqi % // % // >a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"not_eq_to_eqb_false/a normalize // 
+       @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a ??? (a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a ? ? ltin)) // 
+      |#j #ltj #p2j (cases (sub2 j ltj (a href="cic:/matita/basics/bool/andb_true_r.def(4)"andb_true_r/a …p2j))) * 
        #ltkj #p1kj #eqj % // % // 
-       (cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
-       #eqkj @False_ind generalize in match p2j @eqb_elim 
-       normalize /2/
+       (cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a …(a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a …ltkj))) //
+       #eqkj @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a generalize in match p2j; @a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"eqb_elim/a 
+       normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
       ]
-    |>bigop_Sfalse // @(Hind ? len) 
-      [@(transitive_sub … (sub_lt …) sub1) //
+    |>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // @(Hind ? len) 
+      [@(a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"transitive_sub/a … (a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"sub_lt/a …) sub1) //
       |#i #lti #p2i cases(sub2 i lti p2i) * #ltki #p1ki #eqi
-       % // % // cases(le_to_or_lt_eq …(le_S_S_to_le …ltki)) //
-       #eqki @False_ind /2/
+       % // % // cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a …(a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a …ltki)) //
+       #eqki @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.
 
-(* distributivity *)
-
-record Dop (A:Type[0]) (nil:A): Type[0] ≝
-  {sum : ACop A nil; 
-   prod: A → A →A;
-   null: \forall a. prod a nil = nil; 
-   distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
-  }.
-  
-theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.\forall f,a.
-  let aop \def  sum B nil R in
-  let mop \def prod B nil R in
-  mop a \big[aop,nil]_{i<n|p i}(f i) = 
-   \big[aop,nil]_{i<n|p i}(mop a (f i)).
-#n #p #B #nil #R #f #a normalize (elim n) [@null]
-#n #Hind (cases (true_or_false (p n))) #H
-  [>bigop_Strue // >bigop_Strue // >(distr B nil R) >Hind //
-  |>bigop_Sfalse // >bigop_Sfalse //
-  ]
-qed.
-  
-(* Sigma e Pi 
-
-
-notation "Σ_{ ident i < n | p } f"
-  with precedence 80
-for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}.
-
-notation "Σ_{ ident i < n } f"
-  with precedence 80
-for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
-
-notation "Σ_{ ident j ∈ [a,b[ } f"
-  with precedence 80
-for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-  
-notation "Σ_{ ident j ∈ [a,b[ | p } f"
-  with precedence 80
-for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
- 
-notation "Π_{ ident i < n | p} f"
-  with precedence 80
-for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
- 
-notation "Π_{ ident i < n } f"
-  with precedence 80
-for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
-
-notation "Π_{ ident j ∈ [a,b[ } f"
-  with precedence 80
-for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-  
-notation "Π_{ ident j ∈ [a,b[ | p } f"
-  with precedence 80
-for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-
-*)
-(*
-    
-definition p_ord_times \def
-\lambda p,m,x.
-  match p_ord x p with
-  [pair q r \Rightarrow r*m+q].
-  
-theorem  eq_p_ord_times: \forall p,m,x.
-p_ord_times p m x = (ord_rem x p)*m+(ord x p).
-intros.unfold p_ord_times. unfold ord_rem.
-unfold ord.
-elim (p_ord x p).
-reflexivity.
-qed.
-
-theorem div_p_ord_times: 
-\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
-intros.rewrite > eq_p_ord_times.
-apply div_plus_times.
-assumption.
-qed.
-
-theorem mod_p_ord_times: 
-\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
-intros.rewrite > eq_p_ord_times.
-apply mod_plus_times.
-assumption.
-qed.
-
-lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
-intros.
-elim (le_to_or_lt_eq O ? (le_O_n m))
-  [assumption
-  |apply False_ind.
-   rewrite < H1 in H.
-   rewrite < times_n_O in H.
-   apply (not_le_Sn_O ? H)
-  ]
-qed.
-
-theorem iter_p_gen_knm:
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A. 
-(symmetric A plusA) \to 
-(associative A plusA) \to 
-(\forall a:A.(plusA a  baseA) = a)\to
-\forall g: nat \to A.
-\forall h2:nat \to nat \to nat.
-\forall h11,h12:nat \to nat. 
-\forall k,n,m.
-\forall p1,p21:nat \to bool.
-\forall p22:nat \to nat \to bool.
-(\forall x. x < k \to p1 x = true \to 
-p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
-\land h2 (h11 x) (h12 x) = x 
-\land (h11 x) < n \land (h12 x) < m) \to
-(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
-p1 (h2 i j) = true \land 
-h11 (h2 i j) = i \land h12 (h2 i j) = j
-\land h2 i j < k) \to
-iter_p_gen k p1 A g baseA plusA =
-iter_p_gen n p21 A (\lambda x:nat.iter_p_gen m (p22 x) A (\lambda y. g (h2 x y)) baseA plusA) baseA plusA.
-intros.
-rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
-apply sym_eq.
-apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
- [intros.
-  elim (H4 (i/m) (i \mod m));clear H4
-   [elim H7.clear H7.
-    elim H4.clear H4.
-    assumption
-   |apply (lt_times_to_lt_div ? ? ? H5)
-   |apply lt_mod_m_m.
-    apply (lt_times_to_lt_O ? ? ? H5)
-   |apply (andb_true_true ? ? H6)
-   |apply (andb_true_true_r ? ? H6)
-   ]
- |intros.
-  elim (H4 (i/m) (i \mod m));clear H4
-   [elim H7.clear H7.
-    elim H4.clear H4.
-    rewrite > H10.
-    rewrite > H9.
-    apply sym_eq.
-    apply div_mod.
-    apply (lt_times_to_lt_O ? ? ? H5)
-   |apply (lt_times_to_lt_div ? ? ? H5)
-   |apply lt_mod_m_m.
-    apply (lt_times_to_lt_O ? ? ? H5)  
-   |apply (andb_true_true ? ? H6)
-   |apply (andb_true_true_r ? ? H6)
-   ]
- |intros.
-  elim (H4 (i/m) (i \mod m));clear H4
-   [elim H7.clear H7.
-    elim H4.clear H4.
-    assumption
-   |apply (lt_times_to_lt_div ? ? ? H5)
-   |apply lt_mod_m_m.
-    apply (lt_times_to_lt_O ? ? ? H5)
-   |apply (andb_true_true ? ? H6)
-   |apply (andb_true_true_r ? ? H6)
-   ]
- |intros.
-  elim (H3 j H5 H6).
-  elim H7.clear H7.
-  elim H9.clear H9.
-  elim H7.clear H7.
-  rewrite > div_plus_times
-   [rewrite > mod_plus_times
-     [rewrite > H9.
-      rewrite > H12.
-      reflexivity.
-     |assumption
-     ]
-   |assumption
-   ]
- |intros.
-  elim (H3 j H5 H6).
-  elim H7.clear H7.
-  elim H9.clear H9.
-  elim H7.clear H7. 
-  rewrite > div_plus_times
-   [rewrite > mod_plus_times
-     [assumption
-     |assumption
-     ]
-   |assumption
-   ]
- |intros.
-  elim (H3 j H5 H6).
-  elim H7.clear H7.
-  elim H9.clear H9.
-  elim H7.clear H7. 
-  apply (lt_to_le_to_lt ? ((h11 j)*m+m))
-   [apply monotonic_lt_plus_r.
-    assumption
-   |rewrite > sym_plus.
-    change with ((S (h11 j)*m) \le n*m).
-    apply monotonic_le_times_l.
-    assumption
-   ]
- ]
-qed.
-
-theorem iter_p_gen_divides:
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A. 
-\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
-\forall g: nat \to A.
-(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
-
-\to
-
-iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
-iter_p_gen (S n) (\lambda x.divides_b x n) A
-  (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
-intros.
-cut (O < p)
-  [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
-   apply (trans_eq ? ? 
-    (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
-       (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
-    [apply sym_eq.
-     apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
-      [ assumption
-      | assumption
-      | assumption
-      |intros.
-       lapply (divides_b_true_to_lt_O ? ? H H7).
-       apply divides_to_divides_b_true
-        [rewrite > (times_n_O O).
-         apply lt_times
-          [assumption
-          |apply lt_O_exp.assumption
-          ]
-        |apply divides_times
-          [apply divides_b_true_to_divides.assumption
-          |apply (witness ? ? (p \sup (m-i \mod (S m)))).
-           rewrite < exp_plus_times.
-           apply eq_f.
-           rewrite > sym_plus.
-           apply plus_minus_m_m.
-           autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
-          ]
-        ]
-      |intros.
-       lapply (divides_b_true_to_lt_O ? ? H H7).
-       unfold p_ord_times.
-       rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
-        [change with ((i/S m)*S m+i \mod S m=i).
-         apply sym_eq.
-         apply div_mod.
-         apply lt_O_S
-        |assumption
-        |unfold Not.intro.
-         apply H2.
-         apply (trans_divides ? (i/ S m))
-          [assumption|
-           apply divides_b_true_to_divides;assumption]
-        |apply sym_times.
-        ]
-      |intros.
-       apply le_S_S.
-       apply le_times
-        [apply le_S_S_to_le.
-         change with ((i/S m) < S n).
-         apply (lt_times_to_lt_l m).
-         apply (le_to_lt_to_lt ? i);[2:assumption]
-         autobatch by eq_plus_to_le, div_mod, lt_O_S.
-        |apply le_exp
-          [assumption
-          |apply le_S_S_to_le.
-           apply lt_mod_m_m.
-           apply lt_O_S
-          ]
-        ]
-      |intros.
-       cut (ord j p < S m)
-        [rewrite > div_p_ord_times
-          [apply divides_to_divides_b_true
-            [apply lt_O_ord_rem
-             [elim H1.assumption
-             |apply (divides_b_true_to_lt_O ? ? ? H7).
-               rewrite > (times_n_O O).
-               apply lt_times
-               [assumption|apply lt_O_exp.assumption]
-             ]
-           |cut (n = ord_rem (n*(exp p m)) p)
-              [rewrite > Hcut2.
-               apply divides_to_divides_ord_rem
-                [apply (divides_b_true_to_lt_O ? ? ? H7).
-                 rewrite > (times_n_O O).
-                 apply lt_times
-                 [assumption|apply lt_O_exp.assumption]
-                 |rewrite > (times_n_O O).
-                   apply lt_times
-                  [assumption|apply lt_O_exp.assumption]
-               |assumption
-               |apply divides_b_true_to_divides.
-                assumption
-               ]
-              |unfold ord_rem.
-              rewrite > (p_ord_exp1 p ? m n)
-                [reflexivity
-               |assumption
-                |assumption
-               |apply sym_times
-               ]
-             ]
-            ]
-          |assumption
-          ]
-        |cut (m = ord (n*(exp p m)) p)
-          [apply le_S_S.
-           rewrite > Hcut1.
-           apply divides_to_le_ord
-            [apply (divides_b_true_to_lt_O ? ? ? H7).
-             rewrite > (times_n_O O).
-             apply lt_times
-              [assumption|apply lt_O_exp.assumption]
-            |rewrite > (times_n_O O).
-             apply lt_times
-              [assumption|apply lt_O_exp.assumption]
-            |assumption
-            |apply divides_b_true_to_divides.
-             assumption
-            ]
-          |unfold ord.
-           rewrite > (p_ord_exp1 p ? m n)
-            [reflexivity
-            |assumption
-            |assumption
-            |apply sym_times
-            ]
-          ]
-        ]
-      |intros.
-       cut (ord j p < S m)
-        [rewrite > div_p_ord_times
-          [rewrite > mod_p_ord_times
-            [rewrite > sym_times.
-             apply sym_eq.
-             apply exp_ord
-              [elim H1.assumption
-              |apply (divides_b_true_to_lt_O ? ? ? H7).
-               rewrite > (times_n_O O).
-               apply lt_times
-                [assumption|apply lt_O_exp.assumption]
-              ]
-           |cut (m = ord (n*(exp p m)) p)
-             [apply le_S_S.
-              rewrite > Hcut2.
-              apply divides_to_le_ord
-               [apply (divides_b_true_to_lt_O ? ? ? H7).
-                rewrite > (times_n_O O).
-                apply lt_times
-                 [assumption|apply lt_O_exp.assumption]
-               |rewrite > (times_n_O O).
-                apply lt_times
-                 [assumption|apply lt_O_exp.assumption]
-               |assumption
-               |apply divides_b_true_to_divides.
-                assumption
-               ]
-             |unfold ord.
-              rewrite > (p_ord_exp1 p ? m n)
-                [reflexivity
-                |assumption
-                |assumption
-                |apply sym_times
-                ]
-              ]
-            ]
-          |assumption
-          ]
-        |cut (m = ord (n*(exp p m)) p)
-          [apply le_S_S.
-           rewrite > Hcut1.
-           apply divides_to_le_ord
-            [apply (divides_b_true_to_lt_O ? ? ? H7).
-             rewrite > (times_n_O O).
-             apply lt_times
-              [assumption|apply lt_O_exp.assumption]
-            |rewrite > (times_n_O O).
-             apply lt_times
-              [assumption|apply lt_O_exp.assumption]
-            |assumption
-            |apply divides_b_true_to_divides.
-             assumption
-            ]
-          |unfold ord.
-           rewrite > (p_ord_exp1 p ? m n)
-            [reflexivity
-            |assumption
-            |assumption
-            |apply sym_times
-            ]
-          ]
-        ]
-      |intros.
-       rewrite > eq_p_ord_times.
-       rewrite > sym_plus.
-       apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
-        [apply lt_plus_l.
-         apply le_S_S.
-         cut (m = ord (n*(p \sup m)) p)
-          [rewrite > Hcut1.
-           apply divides_to_le_ord
-            [apply (divides_b_true_to_lt_O ? ? ? H7).
-             rewrite > (times_n_O O).
-             apply lt_times
-              [assumption|apply lt_O_exp.assumption]
-            |rewrite > (times_n_O O).
-             apply lt_times
-              [assumption|apply lt_O_exp.assumption]
-            |assumption
-            |apply divides_b_true_to_divides.
-             assumption
-            ]
-          |unfold ord.
-           rewrite > sym_times.
-           rewrite > (p_ord_exp1 p ? m n)
-            [reflexivity
-            |assumption
-            |assumption
-            |reflexivity
-            ]
-          ]
-        |change with (S (ord_rem j p)*S m \le S n*S m).
-         apply le_times_l.
-         apply le_S_S.
-         cut (n = ord_rem (n*(p \sup m)) p)
-          [rewrite > Hcut1.
-           apply divides_to_le
-            [apply lt_O_ord_rem
-              [elim H1.assumption
-              |rewrite > (times_n_O O).
-               apply lt_times
-                [assumption|apply lt_O_exp.assumption]
-              ]
-            |apply divides_to_divides_ord_rem
-              [apply (divides_b_true_to_lt_O ? ? ? H7).
-               rewrite > (times_n_O O).
-               apply lt_times
-                [assumption|apply lt_O_exp.assumption]
-              |rewrite > (times_n_O O).
-               apply lt_times
-                [assumption|apply lt_O_exp.assumption]
-              |assumption
-              |apply divides_b_true_to_divides.
-               assumption
-              ]
-            ]
-        |unfold ord_rem.
-         rewrite > sym_times.
-         rewrite > (p_ord_exp1 p ? m n)
-          [reflexivity
-          |assumption
-          |assumption
-          |reflexivity
-          ]
-        ]
+(* commutation *)
+img class="anchor" src="icons/tick.png" id="bigop_commute"theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a B nil.∀f.
+a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m →
+(∀i,j. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → j a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → (p11 i a title="boolean and" href="cic:/fakeuri.def(1)"∧/a p12 i j) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (p21 j a title="boolean and" href="cic:/fakeuri.def(1)"∧/a p22 i j)) →
+\big[op,nil]_{i<n|p11 ia title="bigop" href="cic:/fakeuri.def(1)"}/a(\big[op,nil]_{j<m|p12 i ja title="bigop" href="cic:/fakeuri.def(1)"}/a(f i j)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+   \big[op,nil]_{j<m|p21 ja title="bigop" href="cic:/fakeuri.def(1)"}/a(\big[op,nil]_{i<n|p22 i ja title="bigop" href="cic:/fakeuri.def(1)"}/a(f i j)).
+#n #m #p11 #p12 #p21 #p22 #B #nil #op #f #posn #posm #Heq
+>a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"bigop_prod/a >a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"bigop_prod/a @a href="cic:/matita/arithmetics/bigops/bigop_iso.def(9)"bigop_iso/a 
+%{(λi.(ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m)a title="natural times" href="cic:/fakeuri.def(1)"*/an a title="natural plus" href="cic:/fakeuri.def(1)"+/a ia title="natural divide" href="cic:/fakeuri.def(1)"//am)} %{(λi.(ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n)a title="natural times" href="cic:/fakeuri.def(1)"*/am a title="natural plus" href="cic:/fakeuri.def(1)"+/a ia title="natural divide" href="cic:/fakeuri.def(1)"//an)} % 
+  [% 
+    [#i #lti #Heq (* whd in ⊢ (???(?(?%?)?)); *) @a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a
+      [@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"mod_plus_times/a /2 by a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a/
+      |@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"div_plus_times/a /2 by a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a/
       ]
-    ]
-  |apply eq_iter_p_gen
-  
-    [intros.
-     elim (divides_b (x/S m) n);reflexivity
-    |intros.reflexivity
-    ]
-  ]
-|elim H1.apply lt_to_le.assumption
-]
-qed.
-    
-
-
-theorem iter_p_gen_2_eq: 
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A. 
-(symmetric A plusA) \to 
-(associative A plusA) \to 
-(\forall a:A.(plusA a  baseA) = a)\to
-\forall g: nat \to nat \to A.
-\forall h11,h12,h21,h22: nat \to nat \to nat. 
-\forall n1,m1,n2,m2.
-\forall p11,p21:nat \to bool.
-\forall p12,p22:nat \to nat \to bool.
-(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
-p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
-\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
-\land h11 i j < n1 \land h12 i j < m1) \to
-(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
-p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
-\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
-\land (h21 i j) < n2 \land (h22 i j) < m2) \to
-iter_p_gen n1 p11 A 
-     (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) 
-     baseA plusA =
-iter_p_gen n2 p21 A 
-    (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
-    baseA plusA.
-
-intros.
-rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
-letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
-letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
-letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
-
-apply (trans_eq ? ? 
-(iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
- (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1))) baseA plusA ) baseA plusA))
-[
-  apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
-  [ elim (and_true ? ? H6).
-    cut(O \lt m1)
-    [ cut(x/m1 < n1)
-      [ cut((x \mod m1) < m1)
-        [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
-          elim H9.clear H9.
-          elim H11.clear H11.
-          elim H9.clear H9.
-          elim H11.clear H11.
-          split
-          [ split
-            [ split
-              [ split
-                [ assumption
-                | assumption
-                ]
-              | unfold ha.
-                unfold ha12.
-                unfold ha22.
-                rewrite > H14.
-                rewrite > H13.
-                apply sym_eq.
-                apply div_mod.
-                assumption
-              ]
-            | assumption
-            ]
-          | assumption
+    |#i #lti #Hi 
+     cut ((ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a ma title="natural times" href="cic:/fakeuri.def(1)"*/ana title="natural plus" href="cic:/fakeuri.def(1)"+/aia title="natural divide" href="cic:/fakeuri.def(1)"//am)a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aia title="natural divide" href="cic:/fakeuri.def(1)"//am)
+      [@a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"mod_plus_times/a @a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a //] #H1
+     cut ((ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a ma title="natural times" href="cic:/fakeuri.def(1)"*/ana title="natural plus" href="cic:/fakeuri.def(1)"+/aia title="natural divide" href="cic:/fakeuri.def(1)"//am)a title="natural divide" href="cic:/fakeuri.def(1)"//ana title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ai a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m)
+      [@a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"div_plus_times/a @a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a //] #H2
+     %[%[@(a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a ? (ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a ma title="natural times" href="cic:/fakeuri.def(1)"*/ana title="natural plus" href="cic:/fakeuri.def(1)"+/an))
+          [whd >a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"plus_n_Sm/a @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a @a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a //
+          |>a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a @(a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m)) m n n) // @a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a //
           ]
-        | apply lt_mod_m_m.
-          assumption
+        |lapply (Heq (ia title="natural divide" href="cic:/fakeuri.def(1)"//am) (i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m) ??)
+          [@a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a // |@a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a //|>Hi >H1 >H2 //]
         ]
-      | apply (lt_times_n_to_lt m1)
-        [ assumption
-        | apply (le_to_lt_to_lt ? x)
-          [ apply (eq_plus_to_le ? ? (x \mod m1)).
-            apply div_mod.
-            assumption
-          | assumption
-        ]
-      ]  
-    ]
-    | apply not_le_to_lt.unfold.intro.
-      generalize in match H5.
-      apply (le_n_O_elim ? H9).
-      rewrite < times_n_O.
-      apply le_to_not_lt.
-      apply le_O_n.              
-    ]
-  | elim (H3 ? ? H5 H6 H7 H8).
-    elim H9.clear H9.
-    elim H11.clear H11.
-    elim H9.clear H9.
-    elim H11.clear H11.
-    cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
-    [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
-      [ split
-        [ split
-          [ split
-            [ apply true_to_true_to_andb_true
-              [ rewrite > Hcut.
-                assumption
-              | rewrite > Hcut1.
-                rewrite > Hcut.
-                assumption
-              ] 
-            | unfold ha.
-              unfold ha12.
-              rewrite > Hcut1.
-              rewrite > Hcut.
-              assumption
-            ]
-          | unfold ha.
-            unfold ha22.
-            rewrite > Hcut1.
-            rewrite > Hcut.
-            assumption            
-          ]
-        | cut(O \lt m1)
-          [ cut(O \lt n1)      
-            [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
-              [ unfold ha.
-                apply (lt_plus_r).
-                assumption
-              | rewrite > sym_plus.
-                rewrite > (sym_times (h11 i j) m1).
-                rewrite > times_n_Sm.
-                rewrite > sym_times.
-                apply (le_times_l).
-                assumption  
-              ]
-            | apply not_le_to_lt.unfold.intro.
-              generalize in match H12.
-              apply (le_n_O_elim ? H11).       
-              apply le_to_not_lt.
-              apply le_O_n
-            ]
-          | apply not_le_to_lt.unfold.intro.
-            generalize in match H10.
-            apply (le_n_O_elim ? H11).       
-            apply le_to_not_lt.
-            apply le_O_n
-          ]  
-        ]
-      | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
-        reflexivity.
-        assumption
-      ]     
-    | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
-      reflexivity.
-      assumption
+      |>H1 >H2 //
+      ]
     ]
-  ]
-| apply (eq_iter_p_gen1)
-  [ intros. reflexivity 
-  | intros.
-    apply (eq_iter_p_gen1)
-    [ intros. reflexivity
-    | intros.
-      rewrite > (div_plus_times)
-      [ rewrite > (mod_plus_times)
-        [ reflexivity
-        | elim (H3 x x1 H5 H7 H6 H8).
-          assumption
+  |#i #lti #Hi 
+   cut ((ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a na title="natural times" href="cic:/fakeuri.def(1)"*/ama title="natural plus" href="cic:/fakeuri.def(1)"+/aia title="natural divide" href="cic:/fakeuri.def(1)"//an)a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a ma title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aia title="natural divide" href="cic:/fakeuri.def(1)"//an)
+    [@a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"mod_plus_times/a @a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a //] #H1
+   cut ((ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a na title="natural times" href="cic:/fakeuri.def(1)"*/ama title="natural plus" href="cic:/fakeuri.def(1)"+/aia title="natural divide" href="cic:/fakeuri.def(1)"//an)a title="natural divide" href="cic:/fakeuri.def(1)"//ama title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ai a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n)
+    [@a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"div_plus_times/a @a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a //] #H2
+   %[%[@(a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a ? (ia title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a na title="natural times" href="cic:/fakeuri.def(1)"*/ama title="natural plus" href="cic:/fakeuri.def(1)"+/am))
+        [whd >a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"plus_n_Sm/a @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a @a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a //
+        |>a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a @(a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n)) n m m) // @a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a //
         ]
-      | elim (H3 x x1 H5 H7 H6 H8).       
-        assumption
+      |lapply (Heq (i a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n) (ia title="natural divide" href="cic:/fakeuri.def(1)"//an) ??)
+        [@a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"lt_times_to_lt_div/a // |@a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a // |>Hi >H1 >H2 //]
       ]
+    |>H1 >H2 //
     ]
   ]
-]
 qed.
 
-theorem iter_p_gen_iter_p_gen: 
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A. 
-(symmetric A plusA) \to 
-(associative A plusA) \to 
-(\forall a:A.(plusA a  baseA) = a)\to
-\forall g: nat \to nat \to A.
-\forall n,m.
-\forall p11,p21:nat \to bool.
-\forall p12,p22:nat \to nat \to bool.
-(\forall x,y. x < n \to y < m \to 
- (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
-iter_p_gen n p11 A 
-  (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA) 
-  baseA plusA =
-iter_p_gen m p21 A 
-  (\lambda y:nat.iter_p_gen n (p22 y) A  (\lambda x. g x y) baseA plusA )
-  baseA plusA.
-intros.
-apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
-       n m m n p11 p21 p12 p22)
-  [intros.split
-    [split
-      [split
-        [split
-          [split
-            [apply (andb_true_true ? (p12 j i)).
-             rewrite > H3
-              [rewrite > H6.rewrite > H7.reflexivity
-              |assumption
-              |assumption
-              ]
-            |apply (andb_true_true_r (p11 j)).
-             rewrite > H3
-              [rewrite > H6.rewrite > H7.reflexivity
-              |assumption
-              |assumption
-              ]
-            ]
-          |reflexivity
-          ]
-        |reflexivity
-        ]
-      |assumption
-      ]
-    |assumption
-    ]
-  |intros.split
-    [split
-      [split
-        [split
-          [split
-            [apply (andb_true_true ? (p22 j i)).
-             rewrite < H3
-              [rewrite > H6.rewrite > H7.reflexivity
-              |assumption
-              |assumption
-              ]
-            |apply (andb_true_true_r (p21 j)).
-             rewrite < H3
-              [rewrite > H6.rewrite > H7.reflexivity
-              |assumption
-              |assumption
-              ]
-            ]
-          |reflexivity
-          ]
-        |reflexivity
-        ]
-      |assumption
-      ]
-    |assumption
-    ]
+(* distributivity *)
+
+img class="anchor" src="icons/tick.png" id="Dop"record Dop (A:Type[0]) (nil:A): Type[0] ≝
+  {sum : a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"ACop/a A nil; 
+   prod: A → A →A;
+   null: \forall a. prod a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a nil; 
+   distr: ∀a,b,c:A. prod a (sum b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a sum (prod a b) (prod a c)
+  }.
+  
+img class="anchor" src="icons/tick.png" id="bigop_distr"theorem bigop_distr: ∀n,p,B,nil.∀R:a href="cic:/matita/arithmetics/bigops/Dop.ind(1,0,2)"Dop/a B nil.\forall f,a.
+  let aop \def  a href="cic:/matita/arithmetics/bigops/sum.fix(0,2,4)"sum/a B nil R in
+  let mop \def a href="cic:/matita/arithmetics/bigops/prod.fix(0,2,4)"prod/a B nil R in
+  mop a \big[aop,nil]_{i<n|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+   \big[aop,nil]_{i<n|p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(mop a (f i)).
+#n #p #B #nil #R #f #a normalize (elim n) [@a href="cic:/matita/arithmetics/bigops/null.fix(0,2,5)"null/a]
+#n #Hind (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p n))) #H
+  [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a // >(a href="cic:/matita/arithmetics/bigops/distr.fix(0,2,5)"distr/a B nil R) >Hind //
+  |>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a // >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a //
   ]
-qed. *)
\ No newline at end of file
+qed.
+  
\ No newline at end of file
diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index 6927d4c99..8c3231ee1 100644
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -11,7 +11,7 @@
 
 include "basics/relations.ma".
 
-img class="anchor" src="icons/tick.png" id="nat"inductive nat : Type[0] ≝
+inductive nat : Type[0] ≝
   | O : nat
   | S : nat → nat.
   
@@ -19,37 +19,37 @@ interpretation "Natural numbers" 'N = nat.
 
 alias num (instance 0) = "natural number".
 
-img class="anchor" src="icons/tick.png" id="pred"definition pred ≝
+definition pred ≝
  λn. match n with [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | S p ⇒ p].
 
-img class="anchor" src="icons/tick.png" id="pred_Sn"theorem pred_Sn : ∀n.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n).
+theorem pred_Sn : ∀n.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n).
 // qed.
 
-img class="anchor" src="icons/tick.png" id="injective_S"theorem injective_S : a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a.
+theorem injective_S : a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a.
 // qed.
 
 (*
 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
 //. qed. *)
 
-img class="anchor" src="icons/tick.png" id="not_eq_S"theorem not_eq_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
+theorem not_eq_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="not_zero"definition not_zero: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
+definition not_zero: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
  λn: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. match n with [ O ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a | (S p) ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a ].
 
-img class="anchor" src="icons/tick.png" id="not_eq_O_S"theorem not_eq_O_S : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
+theorem not_eq_O_S : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
 #n @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #eqOS (change with (a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a)) >eqOS // qed.
 
-img class="anchor" src="icons/tick.png" id="not_eq_n_Sn"theorem not_eq_n_Sn: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
+theorem not_eq_n_Sn: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
 #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="nat_case"theorem nat_case:
+theorem nat_case:
  ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop. 
   (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → P a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) → (∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → P (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) → P n.
 #n #P (elim n) /span class="autotactic"2span class="autotrace" trace /span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="nat_elim2"theorem nat_elim2 :
+theorem nat_elim2 :
  ∀R:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop.
   (∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a n) 
   → (∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a)
@@ -57,18 +57,18 @@ theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
   → ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R n m.
 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /span class="autotactic"2span class="autotrace" trace /span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="decidable_eq_nat"theorem decidable_eq_nat : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am).
+theorem decidable_eq_nat : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am).
 @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n [ (cases n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a/span/span/ | #m #Hind (cases Hind) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/]
 qed. 
 
 (*************************** plus ******************************)
 
-img class="anchor" src="icons/tick.png" id="plus"let rec plus n m ≝ 
+let rec plus n m ≝ 
  match n with [ O ⇒ m | S p ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (plus p m) ].
 
 interpretation "natural plus" 'plus x y = (plus x y).
 
-img class="anchor" src="icons/tick.png" id="plus_O_n"theorem plus_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural plus" href="cic:/fakeuri.def(1)"+/an.
+theorem plus_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural plus" href="cic:/fakeuri.def(1)"+/an.
 // qed.
 
 (*
@@ -76,10 +76,10 @@ theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
 // qed.
 *)
 
-img class="anchor" src="icons/tick.png" id="plus_n_O"theorem plus_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="natural number" href="cic:/fakeuri.def(1)"0/a.
+theorem plus_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="natural number" href="cic:/fakeuri.def(1)"0/a.
 #n (elim n) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="plus_n_Sm"theorem plus_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
+theorem plus_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
 #n (elim n) normalize // qed.
 
 (*
@@ -92,16 +92,16 @@ theorem plus_n_1 : ∀n:nat. S n = n+1.
 // qed.
 *)
 
-img class="anchor" src="icons/tick.png" id="commutative_plus"theorem commutative_plus: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
+theorem commutative_plus: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
 #n (elim n) normalize // qed. 
 
-img class="anchor" src="icons/tick.png" id="associative_plus"theorem associative_plus : a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
+theorem associative_plus : a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
 #n (elim n) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="assoc_plus1"theorem assoc_plus1: ∀a,b,c. c a title="natural plus" href="cic:/fakeuri.def(1)"+/a (b a title="natural plus" href="cic:/fakeuri.def(1)"+/a a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a a.
+theorem assoc_plus1: ∀a,b,c. c a title="natural plus" href="cic:/fakeuri.def(1)"+/a (b a title="natural plus" href="cic:/fakeuri.def(1)"+/a a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a a.
 // qed. 
 
-img class="anchor" src="icons/tick.png" id="injective_plus_r"theorem injective_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am).
+theorem injective_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am).
 #n (elim n) normalize /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a/span/span/ qed.
 
 (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
@@ -115,43 +115,43 @@ theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
 
 (*************************** times *****************************)
 
-img class="anchor" src="icons/tick.png" id="times"let rec times n m ≝ 
+let rec times n m ≝ 
  match n with [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | S p ⇒ ma title="natural plus" href="cic:/fakeuri.def(1)"+/a(times p m) ].
 
 interpretation "natural times" 'times x y = (times x y).
 
-img class="anchor" src="icons/tick.png" id="times_Sn_m"theorem times_Sn_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ma title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural times" href="cic:/fakeuri.def(1)"*/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="natural times" href="cic:/fakeuri.def(1)"*/am.
+theorem times_Sn_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ma title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural times" href="cic:/fakeuri.def(1)"*/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="natural times" href="cic:/fakeuri.def(1)"*/am.
 // qed.
 
-img class="anchor" src="icons/tick.png" id="times_O_n"theorem times_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural times" href="cic:/fakeuri.def(1)"*/an.
+theorem times_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural times" href="cic:/fakeuri.def(1)"*/an.
 // qed.
 
-img class="anchor" src="icons/tick.png" id="times_n_O"theorem times_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
+theorem times_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
 #n (elim n) // qed.
 
-img class="anchor" src="icons/tick.png" id="times_n_Sm"theorem times_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural times" href="cic:/fakeuri.def(1)"*/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m).
+theorem times_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural times" href="cic:/fakeuri.def(1)"*/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m).
 #n (elim n) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="commutative_times"theorem commutative_times : a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. 
+theorem commutative_times : a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. 
 #n (elim n) normalize // qed. 
 
 (* variant sym_times : \forall n,m:nat. n*m = m*n \def
 symmetric_times. *)
 
-img class="anchor" src="icons/tick.png" id="distributive_times_plus"theorem distributive_times_plus : a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
+theorem distributive_times_plus : a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a.
 #n (elim n) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="distributive_times_plus_r"theorem distributive_times_plus_r :
+theorem distributive_times_plus_r :
   ∀a,b,c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. (ba title="natural plus" href="cic:/fakeuri.def(1)"+/ac)a title="natural times" href="cic:/fakeuri.def(1)"*/aa a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ba title="natural times" href="cic:/fakeuri.def(1)"*/aa a title="natural plus" href="cic:/fakeuri.def(1)"+/a ca title="natural times" href="cic:/fakeuri.def(1)"*/aa.
 // qed. 
 
-img class="anchor" src="icons/tick.png" id="associative_times"theorem associative_times: a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a.
+theorem associative_times: a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a.
 #n (elim n) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="times_times"lemma times_times: ∀x,y,z. xa title="natural times" href="cic:/fakeuri.def(1)"*/a(ya title="natural times" href="cic:/fakeuri.def(1)"*/az) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ya title="natural times" href="cic:/fakeuri.def(1)"*/a(xa title="natural times" href="cic:/fakeuri.def(1)"*/az).
+lemma times_times: ∀x,y,z. xa title="natural times" href="cic:/fakeuri.def(1)"*/a(ya title="natural times" href="cic:/fakeuri.def(1)"*/az) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ya title="natural times" href="cic:/fakeuri.def(1)"*/a(xa title="natural times" href="cic:/fakeuri.def(1)"*/az).
 // qed. 
 
-img class="anchor" src="icons/tick.png" id="times_n_1"theorem times_n_1 : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural times" href="cic:/fakeuri.def(1)"*/a a title="natural number" href="cic:/fakeuri.def(1)"1/a.
+theorem times_n_1 : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural times" href="cic:/fakeuri.def(1)"*/a a title="natural number" href="cic:/fakeuri.def(1)"1/a.
 #n // qed.
 
 (* ci servono questi risultati? 
@@ -182,7 +182,7 @@ qed.
 
 (******************** ordering relations ************************)
 
-img class="anchor" src="icons/tick.png" id="le"inductive le (n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
+inductive le (n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
   | le_n : le n n
   | le_S : ∀ m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. le n m → le n (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m).
 
@@ -190,7 +190,7 @@ interpretation "natural 'less or equal to'" 'leq x y = (le x y).
 
 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
 
-img class="anchor" src="icons/tick.png" id="lt"definition lt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+definition lt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 
 interpretation "natural 'less than'" 'lt x y = (lt x y).
 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
@@ -198,16 +198,16 @@ interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
 (* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
 // qed. *)
 
-img class="anchor" src="icons/tick.png" id="ge"definition ge: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+definition ge: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 
 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
 
-img class="anchor" src="icons/tick.png" id="gt"definition gt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.ma title="natural 'less than'" href="cic:/fakeuri.def(1)"</an.
+definition gt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.ma title="natural 'less than'" href="cic:/fakeuri.def(1)"</an.
 
 interpretation "natural 'greater than'" 'gt x y = (gt x y).
 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
 
-img class="anchor" src="icons/tick.png" id="transitive_le"theorem transitive_le : a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a.
+theorem transitive_le : a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a.
 #a #b #c #leab #lebc (elim lebc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/
 qed.
 
@@ -215,29 +215,29 @@ qed.
 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
 \def transitive_le. *)
 
-img class="anchor" src="icons/tick.png" id="transitive_lt"theorem transitive_lt: a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a.
+theorem transitive_lt: a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a.
 #a #b #c #ltab #ltbc (elim ltbc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/qed.
 
 (*
 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
 \def transitive_lt. *)
 
-img class="anchor" src="icons/tick.png" id="le_S_S"theorem le_S_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
+theorem le_S_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m.
 #n #m #lenm (elim lenm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_O_n"theorem le_O_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+theorem le_O_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_n_Sn"theorem le_n_Sn : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
+theorem le_n_Sn : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_pred_n"theorem le_pred_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+theorem le_pred_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 #n (elim n) // qed.
 
-img class="anchor" src="icons/tick.png" id="monotonic_pred"theorem monotonic_pred: a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a ? a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a.
+theorem monotonic_pred: a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a ? a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a.
 #n #m #lenm (elim lenm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed.
 
-img class="anchor" src="icons/tick.png" id="le_S_S_to_le"theorem le_S_S_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
+theorem le_S_S_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 (* demo *)
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed.
 
@@ -248,26 +248,26 @@ theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
 /2/ qed. *)
 
-img class="anchor" src="icons/tick.png" id="lt_to_not_zero"theorem lt_to_not_zero : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a m.
+theorem lt_to_not_zero : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a m.
 #n #m #Hlt (elim Hlt) // qed.
 
 (* lt vs. le *)
-img class="anchor" src="icons/tick.png" id="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.
+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 +275,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 +286,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 +379,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 +394,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 +423,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 +435,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 +444,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 +452,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 +488,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 +496,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_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 +515,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 +535,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,7 +621,7 @@ 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
@@ -692,12 +630,12 @@ qed. *)
   ]
 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(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))
@@ -706,18 +644,18 @@ qed.
   ]
 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.
+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 +705,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 +715,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 +748,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 +761,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 +838,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,52 +847,57 @@ 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(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.
+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.
+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(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.
+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.
+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.
+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(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(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(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 // 
@@ -963,7 +906,7 @@ qed.
   @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
@@ -979,7 +922,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 +932,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 +947,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 +971,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 +981,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,40 +1023,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.
\ No newline at end of file
diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index 43f0f8d05..7762657ae 100644
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -16,7 +16,6 @@ include "basics/relations.ma".
   | true : bool
   | false : bool.
 
-(* destruct does not work *)
 img class="anchor" src="icons/tick.png" id="not_eq_true_false"theorem not_eq_true_false : a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq change with match a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a with [true ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a|false ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a]
 >Heq // qed.
@@ -55,6 +54,10 @@ interpretation "boolean and" 'and x y = (andb x y).
 match b1 with [ true ⇒ P b2 | false ⇒ P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] → P (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
+img class="anchor" src="icons/tick.png" id="true_to_andb_true"theorem true_to_andb_true: ∀b1,b2. b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#b1 cases b1 normalize //
+qed.
+
 img class="anchor" src="icons/tick.png" id="andb_true_l"theorem andb_true_l: ∀ b1,b2. (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #b1 (cases b1) normalize // qed.
 
@@ -102,4 +105,4 @@ notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp
 
 img class="anchor" src="icons/tick.png" id="true_or_false"theorem true_or_false:
 ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
-#b (cases b) /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/ qed.
+#b (cases b) /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/ qed.
\ No newline at end of file