From adfe97c3044e996cc691d760578ba6c91ce386bd Mon Sep 17 00:00:00 2001
From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 31 May 2013 09:36:04 +0000
Subject: [PATCH] Nuovi files

---
 weblib/arithmetics/minimization.ma | 294 +++++++++++++++--------------
 weblib/arithmetics/pidgeon_hole.ma | 112 +++++------
 weblib/basics/append.ma            |   1 -
 3 files changed, 207 insertions(+), 200 deletions(-)
 delete mode 100644 weblib/basics/append.ma

diff --git a/weblib/arithmetics/minimization.ma b/weblib/arithmetics/minimization.ma
index 2959d0f3d..afa47f76b 100644
--- a/weblib/arithmetics/minimization.ma
+++ b/weblib/arithmetics/minimization.ma
@@ -13,7 +13,7 @@ include "arithmetics/nat.ma".
 
 (* maximization *)
 
-let rec max' i f d ≝
+img class="anchor" src="icons/tick.png" id="max'"let rec max' i f d ≝
   match i with 
   [ O ⇒ d
   | S j ⇒ 
@@ -21,123 +21,123 @@ let rec max' i f d ≝
       [ true ⇒ j
       | false ⇒ max' j f d]].
       
-definition max ≝ λn.λf.max' n f O.
+img class="anchor" src="icons/tick.png" id="max"definition max ≝ λn.λf.a href="cic:/matita/arithmetics/minimization/max'.fix(0,0,1)"max'/a n f a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
 
-theorem max_O: ∀f. A href="cic:/matita/arithmetics/minimization/max.def(2)"max/A O f = O.
+img class="anchor" src="icons/tick.png" id="max_O"theorem max_O: ∀f. a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
 // qed.
 
-theorem max_cases: ∀f.∀n.
-  (f n = true ∧ max (S n) f = n) ∨ 
-  (f n  = false ∧ max (S n) f = max n f).
-#f #n normalize cases (f n) normalize /3/ qed.
+img class="anchor" src="icons/tick.png" id="max_cases"theorem max_cases: ∀f.∀n.
+  (f 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 a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n) a title="logical or" href="cic:/fakeuri.def(1)"∨/a 
+  (f n  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 and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f).
+#f #n normalize cases (f n) normalize /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/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed.
 
-theorem le_max_n: ∀f.∀n. max n f ≤ n.
+img class="anchor" src="icons/tick.png" id="le_max_n"theorem le_max_n: ∀f.∀n. a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"max/a n f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 #f #n (elim n) // #m #Hind 
-normalize (cases (f m)) normalize @le_S // 
+normalize (cases (f m)) normalize @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a // 
 (* non trova Hind *)
 @Hind
 qed.
 
-theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
-#f #n #posn @(lt_O_n_elim ? posn) #m
-normalize (cases (f m)) normalize apply le_S_S //
+img class="anchor" src="icons/tick.png" id="lt_max_n"theorem lt_max_n : ∀f.∀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 n → a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"max/a n f a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n.
+#f #n #posn @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a ? posn) #m
+normalize (cases (f m)) normalize font class="Apple-style-span" color="#FF0000"@/fonta href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a //
 @le_max_n qed.
 
-theorem le_to_le_max : ∀f.∀n,m.
-n ≤ m  → max n f ≤ max m f.
+img class="anchor" src="icons/tick.png" id="le_to_le_max"theorem le_to_le_max : ∀f.∀n,m.
+n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m  → a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"max/a m f.
 #f #n #m #H (elim H) //
-#i #leni #Hind @(transitive_le … Hind)
-(cases (max_cases f i)) * #_ /2/ 
+#i #leni #Hind @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … Hind)
+(cases (a href="cic:/matita/arithmetics/minimization/max_cases.def(3)"max_cases/a f i)) * #_ /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ 
 qed.
 
-theorem true_to_le_max: ∀f.∀n,m.
- m < n → f m = true → m ≤ max n f.
+img class="anchor" src="icons/tick.png" id="true_to_le_max"theorem true_to_le_max: ∀f.∀n,m.
+ m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f 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 → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f.
 #f #n (elim n)
-  [#m #ltmO @False_ind /2/
+  [#m #ltmO @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/
   |#i #Hind #m #ltm 
-   (cases (le_to_or_lt_eq … (le_S_S_to_le … ltm)))
-    [#ltm #fm @(transitive_le ? (max i f)) 
-      [@Hind /2/ | @le_to_le_max //]
+   (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 … ltm)))
+    [#ltm #fm @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a i f)) 
+      [@Hind /span class="autotactic"2span class="autotrace" trace /span/span/ | @a href="cic:/matita/arithmetics/minimization/le_to_le_max.def(4)"le_to_le_max/a //]
     |#eqm >eqm #eqf normalize >eqf //
  ] 
 qed.
 
-theorem lt_max_to_false: ∀f.∀n,m.
- m < n → max n f < m → f m = false.
-#f #n #m #ltnm #eqf cases(true_or_false (f m)) //
-#fm @False_ind @(absurd … eqf) @(le_to_not_lt) @true_to_le_max //
+img class="anchor" src="icons/tick.png" id="lt_max_to_false"theorem lt_max_to_false: ∀f.∀n,m.
+ m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → f 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.
+#f #n #m #ltnm #eqf cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f m)) //
+#fm @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 … eqf) @(a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a) @a href="cic:/matita/arithmetics/minimization/true_to_le_max.def(6)"true_to_le_max/a //
 qed.
 
-lemma max_exists: ∀f.∀n,m.m < n → f m =true →
- (∀i. m < i → i < n → f i = false) → max n f = m.
+img class="anchor" src="icons/tick.png" id="max_exists"lemma max_exists: ∀f.∀n,m.m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
+ (∀i. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f 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 href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
 #f #n (elim n) #m
-  [#ltO @False_ind /2/ 
+  [#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/ 
   |#Hind #max #ltmax #fmax #ismax
-   cases (le_to_or_lt_eq …(le_S_S_to_le …(ltmax …)))
+   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 …(ltmax …)))
    #ltm normalize 
      [>(ismax m …) // normalize @(Hind max ltm fmax)
-      #i #Hl #Hr @ismax // @le_S //
+      #i #Hl #Hr @ismax // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //
      |<ltm >fmax // 
      ]
    ]
 qed.
 
-lemma max_not_exists: ∀f.∀n.
- (∀i. i < n → f i = false) → max n f = O.
-#f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj
-normalize >ffalse // @Hind /2/
+img class="anchor" src="icons/tick.png" id="max_not_exists"lemma max_not_exists: ∀f.∀n.
+ (∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f 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 href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
+#f #n #ffalse @(a href="cic:/matita/arithmetics/nat/le_gen.def(1)"le_gen/a ? n) #i (elim i) // #j #Hind #ltj
+normalize >ffalse // @Hind /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/
 qed.
 
-lemma fmax_false: ∀f.∀n,m.max n f = m → f m = false → m = O. 
+img class="anchor" src="icons/tick.png" id="fmax_false"lemma fmax_false: ∀f.∀n,m.a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m → f 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 → m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. 
 #f #n #m (elim n) //
-#i #Hind normalize cases(true_or_false … (f i)) #fi >fi
+#i #Hind normalize cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (f i)) #fi >fi
 normalize 
-  [#eqm #fm @False_ind @(absurd … fi) // |@Hind]
+  [#eqm #fm @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 … fi) // |@Hind]
 qed. 
   
-inductive max_spec (n:nat) (f:nat→bool) : nat→Prop ≝
- | found : ∀m:nat.m < n → f m =true →
- (∀i. m < i → i < n → f i = false) → max_spec n f m
- | not_found: (∀i.i < n → f i = false) → max_spec n f O.
+img class="anchor" src="icons/tick.png" id="max_spec"inductive max_spec (n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (f: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 href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→Prop ≝
+ | found : ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
+ (∀i. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f 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) → max_spec n f m
+ | not_found: (∀i.i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f 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) → max_spec n f a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
  
-theorem max_spec_to_max: ∀f.∀n,m.
-  max_spec n f m → max n f = m.
+img class="anchor" src="icons/tick.png" id="max_spec_to_max"theorem max_spec_to_max: ∀f.∀n,m.
+  a href="cic:/matita/arithmetics/minimization/max_spec.ind(1,0,2)"max_spec/a n f m → a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
 #f #n #m #spec (cases spec) 
-  [#max #ltmax #fmax #ismax @max_exists // @ismax
-  |#ffalse @max_not_exists @ffalse
+  [#max #ltmax #fmax #ismax @a href="cic:/matita/arithmetics/minimization/max_exists.def(6)"max_exists/a // @ismax
+  |#ffalse @a href="cic:/matita/arithmetics/minimization/max_not_exists.def(9)"max_not_exists/a @ffalse
   ] 
 qed.
 
-theorem max_to_max_spec: ∀f.∀n,m.
-  max n f = m → max_spec n f m.
+img class="anchor" src="icons/tick.png" id="max_to_max_spec"theorem max_to_max_spec: ∀f.∀n,m.
+  a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m → a href="cic:/matita/arithmetics/minimization/max_spec.ind(1,0,2)"max_spec/a n f m.
 #f #n #m (cases n)
-  [#eqm <eqm %2 #i #ltiO @False_ind /2/ 
-  |#n #eqm cases(true_or_false (f m)) #fm
+  [#eqm <eqm %2 #i #ltiO @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 #eqm cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f m)) #fm
     (* non trova max_to_false *)
-    [%1 /2/
-    |lapply (fmax_false ??? eqm fm) #eqmO >eqmO
-     %2 #i (cases i) // #j #ltj @(lt_max_to_false … ltj) //
+    [%1 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/minimization/lt_max_n.def(5)"lt_max_n/a, a href="cic:/matita/arithmetics/minimization/lt_max_to_false.def(9)"lt_max_to_false/a/span/span/
+    |lapply (a href="cic:/matita/arithmetics/minimization/fmax_false.def(4)"fmax_false/a ??? eqm fm) #eqmO >eqmO
+     %2 #i (cases i) // #j #ltj @(a href="cic:/matita/arithmetics/minimization/lt_max_to_false.def(9)"lt_max_to_false/a … ltj) //
 qed.
 
-theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) → 
-  max n f = max n g.
+img class="anchor" src="icons/tick.png" id="max_f_g"theorem max_f_g: ∀f,g,n.(∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g i) → 
+  a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n g.
 #f #g #n (elim n) //
-#m #Hind #ext normalize >ext >Hind //
-#i #ltim @ext /2/
+#m #Hind #ext whd in ⊢(??%%); >ext // normalize in Hind; >Hind //
+# i #ltim @ext /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a/span/span/
 qed.
 
-theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) →
-max n f ≤ max n g.
+img class="anchor" src="icons/tick.png" id="le_max_f_max_g"theorem le_max_f_max_g: ∀f,g,n. (∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f 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 → g i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) →
+a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n g.
 #f #g #n (elim n) //
-#m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq 
+#m #Hind #ext normalize (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f m))) #Heq >Heq 
   [>ext //
-  |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/
+  |(cases (g m)) normalize [@a href="cic:/matita/arithmetics/minimization/le_max_n.def(3)"le_max_n/a] @Hind #i #ltim @ext /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a/span/span/
 qed.
 
-theorem f_max_true : ∀ f.∀n.
-(∃i:nat. i < n ∧ f i = true) → f (max n f) = true. 
-#f #n cases(max_to_max_spec f n (max n f) (refl …)) //
-#Hall * #x * #ltx #fx @False_ind @(absurd … fx) >Hall /2/
+img class="anchor" src="icons/tick.png" id="f_max_true"theorem f_max_true : ∀ f.∀n.
+(∃i:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/aa title="exists" href="cic:/fakeuri.def(1)"./a i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a f 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 (a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f) 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 #n cases(a href="cic:/matita/arithmetics/minimization/max_to_max_spec.def(10)"max_to_max_spec/a f n (a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f) (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a …)) //
+#Hall * #x * #ltx #fx @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 … fx) >Hall /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/
 qed.
 
 (* minimization *)
@@ -145,26 +145,26 @@ qed.
 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;  
    returns  b + k otherwise *)
    
-let rec min k b f ≝
+img class="anchor" src="icons/tick.png" id="min"let rec min k b f ≝
   match k with
   [ O ⇒ b
   | S p ⇒ 
     match f b with
    [ true ⇒ b
-   | false ⇒ min p (S b) f]].
+   | false ⇒ min p (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b) f]].
 
-definition min0 ≝ λn.λf. min n 0 f.
+img class="anchor" src="icons/tick.png" id="min0"definition min0 ≝ λn.λf. a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n a title="natural number" href="cic:/fakeuri.def(1)"0/a f.
 
-theorem min_O_f : ∀f.∀b. min O b f = b.
+img class="anchor" src="icons/tick.png" id="min_O_f"theorem min_O_f : ∀f.∀b. a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b.
 // qed.
 
-theorem true_min: ∀f.∀b.
-  f b = true → ∀n.min n b f = b.
+img class="anchor" src="icons/tick.png" id="true_min"theorem true_min: ∀f.∀b.
+  f 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 → ∀n.a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b.
 #f #b #fb #n (cases n) // #n normalize >fb normalize //
 qed.
 
-theorem false_min: ∀f.∀n,b.
-  f b = false → min (S n) b f = min n (S b) f.
+img class="anchor" src="icons/tick.png" id="false_min"theorem false_min: ∀f.∀n,b.
+  f 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 → a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b) f.
 #f #n #b #fb normalize >fb normalize //
 qed.
 
@@ -174,131 +174,139 @@ b1 ≤ b2  → min n b1 f ≤ min n b2 f.
 #f #n #b1 #b2 #leb (elim n) //
 #m #Hind normalize (cases (f m)) normalize *)
 
-theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b.
+img class="anchor" src="icons/tick.png" id="le_min_r"theorem le_min_r: ∀f.∀n,b. a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b.
 #f #n normalize (elim n) // #m #Hind #b 
 normalize (cases (f b)) normalize // 
 qed.
 
-theorem le_min_l: ∀f.∀n,b. b ≤ min n b f.
+img class="anchor" src="icons/tick.png" id="le_min_l"theorem le_min_l: ∀f.∀n,b. b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f.
 #f #n normalize (elim n) // #m #Hind #b 
-normalize (cases (f b)) normalize /2/ 
+normalize (cases (f b)) normalize /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/le.con(0,1,1)"le_n/a/span/span/ 
 qed.
 
-theorem le_to_le_min : ∀f.∀n,m.
-n ≤ m  → ∀b.min n b f ≤ min m b f.
-#f @nat_elim2 //
-  [#n #leSO @False_ind /2/ 
+img class="anchor" src="icons/tick.png" id="le_to_le_min"theorem le_to_le_min : ∀f.∀n,m.
+n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m  → ∀b.a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a m b f.
+#f @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a //
+  [#n #leSO @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 #m #Hind #leSS #b
-   (cases (true_or_false (f b))) #fb 
-    [lapply (true_min …fb) #H >H >H //
-    |>false_min // >false_min // @Hind /2/
+   (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b))) #fb 
+    [lapply (a href="cic:/matita/arithmetics/minimization/true_min.def(4)"true_min/a …fb) #H >H >H //
+    |>a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a // >a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a // @Hind /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/
     ]
   ]
 qed.
 
-theorem true_to_le_min: ∀f.∀n,m,b.
- b ≤ m → f m = true → min n b f ≤ m.
+img class="anchor" src="icons/tick.png" id="true_to_le_min"theorem true_to_le_min: ∀f.∀n,m,b.
+ b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → f 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 → a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 #f #n (elim n) //
-#i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb))
+#i #Hind #m #b #leb (cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … leb))
   [#ltm #fm normalize (cases (f b)) normalize // @Hind //
   |#eqm <eqm #eqb normalize >eqb normalize //
   ] 
 qed.
 
-theorem lt_min_to_false: ∀f.∀n,m,b. 
- b ≤ m → m < min n b f → f m = false.
-#f #n #m #b #lebm #ltm cases(true_or_false (f m)) //
-#fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min //
+img class="anchor" src="icons/tick.png" id="lt_min_to_false"theorem lt_min_to_false: ∀f.∀n,m,b. 
+ b 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 a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f → f 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.
+#f #n #m #b #lebm #ltm cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f m)) //
+#fm @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 … ltm) @(a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a) @a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"true_to_le_min/a //
 qed.
 
-theorem fmin_true: ∀f.∀n,m,b.
- m = min n b f → m < n + b → f m = true. 
+img class="anchor" src="icons/tick.png" id="fmin_true"theorem fmin_true: ∀f.∀n,m,b.
+ m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → f 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. 
 #f #n (elim n)
-  [#m #b normalize #eqmb >eqmb #leSb @(False_ind) 
-   @(absurd … leSb) //
-  |#n #Hind #m #b (cases (true_or_false (f b))) #caseb
-    [>true_min //
-    |>false_min // #eqm #ltm @(Hind m (S b)) /2/
+  [#m #b normalize #eqmb >eqmb #leSb @(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 … leSb) //
+  |#n #Hind #m #b (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b))) #caseb
+    [>a href="cic:/matita/arithmetics/minimization/true_min.def(4)"true_min/a //
+    |>a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a // #eqm #ltm @(Hind m (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b)) /span class="autotactic"2span class="autotrace" trace /span/span/
     ]
   ]
 qed.
 
-lemma min_exists: ∀f.∀t,m. m < t → f m = true →
-∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b → 
-  min k b f = m. 
+img class="anchor" src="icons/tick.png" id="min_exists"lemma min_exists: ∀f.∀t,m. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a t → f 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 →
+∀k,b.b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → (∀i. b 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 m → f 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) → t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a k a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → 
+  a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a k b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m. 
 #f #t #m #ltmt #fm #k (elim k)
-  [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
-   @lt_to_not_le //
-  |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
-    [#ltbm >false_min /2/ @Hind // 
-      [#i #H #H1 @ismin /2/ | >eqt normalize //]
-    |#eqbm >true_min //
+  [#b #lebm #ismin #eqtb @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 … lebm) <eqtb
+   @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a //
+  |#d #Hind #b #lebm #ismin #eqt cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a …lebm)
+    [#ltbm >a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ @Hind // 
+      [#i #H #H1 @ismin /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ | >eqt normalize //]
+    |#eqbm >a href="cic:/matita/arithmetics/minimization/true_min.def(4)"true_min/a //
     ]
   ]
 qed.
 
-lemma min_not_exists: ∀f.∀n,b.
- (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
+img class="anchor" src="icons/tick.png" id="min_not_exists"lemma min_not_exists: ∀f.∀n,b.
+ (∀i. b 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 n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → f 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 href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b.
 #f #n (elim n) // 
-#p #Hind #b #ffalse >false_min
-  [>Hind // #i #H #H1 @ffalse /2/
+#p #Hind #b #ffalse >a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a
+  [>Hind // #i #H #H1 @ffalse /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/
   |@ffalse //
   ]
 qed.
 
-lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in 
- f m = false → m = n+b. 
+img class="anchor" src="icons/tick.png" id="fmin_false"lemma fmin_false: ∀f.∀n,b.let m ≝ a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f in 
+ f 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 → m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/ab. 
 #f #n (elim n) //
-#i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb
+#i #Hind #b normalize cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (f b)) #fb >fb
 normalize 
-  [#eqm @False_ind @(absurd … fb) // 
-  |>plus_n_Sm @Hind]
+  [#eqm @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 … fb) // 
+  |>a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"plus_n_Sm/a @Hind]
 qed.
 
-inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
- | found : ∀m:nat. b ≤ m → m < n + b → f m =true →
- (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m
- | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b).
+img class="anchor" src="icons/tick.png" id="min_spec"inductive min_spec (n,b:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (f: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 href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→Prop ≝
+ | found : ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. b 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 n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
+     (∀i. b 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 m → f 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) → min_spec n b f m
+ | not_found: (∀i.b 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 (n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b) → f 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) → 
+     min_spec n b f (na title="natural plus" href="cic:/fakeuri.def(1)"+/ab).
  
-theorem min_spec_to_min: ∀f.∀n,b,m.
-  min_spec n b f m → min n b f = m.
+img class="anchor" src="icons/tick.png" id="min_spec_to_min"theorem min_spec_to_min: ∀f.∀n,b,m.
+  a href="cic:/matita/arithmetics/minimization/min_spec.ind(1,0,3)"min_spec/a n b f m → a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
 #f #n #b #m #spec (cases spec) 
-  [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin
-  |#ffalse @min_not_exists @ffalse
+  [#m #lem #ltm #fm #ismin @(a href="cic:/matita/arithmetics/minimization/min_exists.def(9)"min_exists/a f (na title="natural plus" href="cic:/fakeuri.def(1)"+/ab)) // @ismin
+  |#ffalse @a href="cic:/matita/arithmetics/minimization/min_not_exists.def(9)"min_not_exists/a @ffalse
   ] 
 qed.
 
-theorem min_to_min_spec: ∀f.∀n,b,m.
-  min n b f = m → min_spec n b f m.
+img class="anchor" src="icons/tick.png" id="min_to_min_spec"theorem min_to_min_spec: ∀f.∀n,b,m.
+  a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m → a href="cic:/matita/arithmetics/minimization/min_spec.ind(1,0,3)"min_spec/a n b f m.
 #f #n #b #m (cases n)
-  [#eqm <eqm %2 #i #lei #lti @False_ind @(absurd … lti) /2/
+  [#eqm <eqm %2 #i #lei #lti @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 … lti) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a/span/span/
   |#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
-   lapply (le_min_r f (S n) b) >eqm #lem
-   (cases (le_to_or_lt_eq … lem)) #mcase
-    [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) //
-    |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) //
+   lapply (a href="cic:/matita/arithmetics/minimization/le_min_r.def(9)"le_min_r/a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) b) >eqm #lem
+   (cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lem)) #mcase
+    [%1 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/minimization/fmin_true.def(7)"fmin_true/a/span/span/ #i #H #H1 @(a href="cic:/matita/arithmetics/minimization/lt_min_to_false.def(9)"lt_min_to_false/a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) i b) //
+    |>mcase %2 #i #lebi #lti @(a href="cic:/matita/arithmetics/minimization/lt_min_to_false.def(9)"lt_min_to_false/a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) i b) //
     ]
   ]
 qed.
 
-theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) → 
-  min n b f = min n b g.
+img class="anchor" src="icons/tick.png" id="min_f_g"theorem min_f_g: ∀f,g,n,b.(∀i. b 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 n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g i) → 
+  a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b g.
 #f #g #n (elim n) //
-#m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
-#i #ltib #ltim @ext /2/
+#m #Hind #b #ext normalize >(ext b (a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a b) ?) // >Hind //
+#i #ltib #ltim @ext /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/
 qed.
 
-theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
-min n b g ≤ min n b f.
+img class="anchor" src="icons/tick.png" id="le_min_f_min_g"theorem le_min_f_min_g: ∀f,g,n,b. 
+  (∀i. b 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 n a title="natural plus" href="cic:/fakeuri.def(1)"+/ab → f 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 → g i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) →
+  a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b g a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f.
 #f #g #n (elim n) //
-#m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq 
+#m #Hind #b #ext normalize (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b))) #Heq >Heq 
   [>ext //
-  |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
-    @ext /2/
+  |(cases (g b)) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ @Hind #i #ltb #ltim #fi
+    @ext /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/
 qed.
 
-theorem f_min_true : ∀ f.∀n,b.
-(∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true. 
-#f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
-#Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
+img class="anchor" src="icons/tick.png" id="f_min_true"theorem f_min_true : ∀ f.∀n,b.
+(∃i:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/aa title="exists" href="cic:/fakeuri.def(1)"./a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i a title="logical and" href="cic:/fakeuri.def(1)"∧/a i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="logical and" href="cic:/fakeuri.def(1)"∧/a f 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 (a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f) 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 #n #b cases(a href="cic:/matita/arithmetics/minimization/min_to_min_spec.def(10)"min_to_min_spec/a f n b (a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f) (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a …)) //
+#Hall * #x * * #leb #ltx #fx @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 … fx) >Hall /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/
+qed.
+
+img class="anchor" src="icons/tick.png" id="lt_min"theorem lt_min : ∀ f.∀n,b.
+(∃i:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/aa title="exists" href="cic:/fakeuri.def(1)"./a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i a title="logical and" href="cic:/fakeuri.def(1)"∧/a i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="logical and" href="cic:/fakeuri.def(1)"∧/a f 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/minimization/min.fix(0,0,1)"min/a n b f a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b. 
+#f #n #b #H cases H #i * * #lebi #ltin #fi_true  
+@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a … ltin) @a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"true_to_le_min/a //
 qed.
diff --git a/weblib/arithmetics/pidgeon_hole.ma b/weblib/arithmetics/pidgeon_hole.ma
index e4aed1629..c7c1f7016 100644
--- a/weblib/arithmetics/pidgeon_hole.ma
+++ b/weblib/arithmetics/pidgeon_hole.ma
@@ -1,89 +1,89 @@
 
 include "arithmetics/bounded_quantifiers.ma".
-include "basics/list.ma".
+include "basics/lists/search.ma".
 
 (* A bit of combinatorics *)
 interpretation "list membership" 'mem a l = (mem ? a l).
 
-lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l).
+img class="anchor" src="icons/tick.png" id="decidable_mem_nat"lemma decidable_mem_nat: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀l. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (n a title="list membership" href="cic:/fakeuri.def(1)"∈/a l).
 #n #l elim l
-  [%2 % @False_ind |#a #tl #Htl @decidable_or //]
+  [%2 % @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a |#a #tl #Htl @a href="cic:/matita/arithmetics/bounded_quantifiers/decidable_or.def(3)"decidable_or/a //]
 qed.
 
-lemma length_unique_le: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| ≤ n.
+img class="anchor" src="icons/tick.png" id="length_unique_le"lemma length_unique_le: ∀n,l. a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l  → (∀x. x a title="list membership" href="cic:/fakeuri.def(1)"∈/a l → x a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n) → |la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 #n elim n 
-  [* // #a #tl #_ #H @False_ind @(absurd (a < 0)) 
-    [@H %1 % | @le_to_not_lt //]
-  |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l)
-   lapply (length_filter_eqb … m l Huni) #Hle
-   @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|))
-    [@le_plus // 
-    |@le_S_S @Hind
-      [@unique_filter // 
-      |#x #memx cut (x ≤ m)
-        [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut
-       cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind
-       @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq
-       @injective_notb @(mem_filter_true ???? memx)
+  [* // #a #tl #_ #H @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 a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="natural number" href="cic:/fakeuri.def(1)"0/a)) 
+    [@H %1 % | @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a //]
+  |#m #Hind #l #Huni #Hmem <(a href="cic:/matita/basics/lists/search/filter_length2.def(5)"filter_length2/a ? (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m) l)
+   lapply (a href="cic:/matita/basics/lists/search/length_filter_eqb.def(8)"length_filter_eqb/a … m l Huni) #Hle
+   @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (a title="natural number" href="cic:/fakeuri.def(1)"1/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a ? (λx.a title="boolean not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m x) la title="list length" href="cic:/fakeuri.def(1)"|/a))
+    [@a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a // 
+    |@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a @Hind
+      [@a href="cic:/matita/basics/lists/search/unique_filter.def(4)"unique_filter/a // 
+      |#x #memx cut (x a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m)
+        [@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @Hmem @(a href="cic:/matita/basics/lists/search/mem_filter.def(3)"mem_filter/a … memx)] #Hcut
+       cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … Hcut) // #eqxm @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 ? eqxm) @a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a @a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"eqb_false_to_not_eq/a
+       @a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a @(a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"mem_filter_true/a ???? memx)
       ]
     ]
   ]
 qed.    
 
-lemma eq_length_to_mem : ∀n,l. |l| = S n → unique ? l → 
-  (∀x. x ∈ l → x ≤ n) → n ∈ l.
-#n #l #H1 #H2 #H3 cases (decidable_mem_nat n l) // 
-#H4 @False_ind @(absurd (|l| > n))
+img class="anchor" src="icons/tick.png" id="eq_length_to_mem"lemma eq_length_to_mem : ∀n,l. |la title="list length" href="cic:/fakeuri.def(1)"|/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 href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l → 
+  (∀x. x a title="list membership" href="cic:/fakeuri.def(1)"∈/a l → x a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n) → n a title="list membership" href="cic:/fakeuri.def(1)"∈/a l.
+#n #l #H1 #H2 #H3 cases (a href="cic:/matita/arithmetics/pidgeon_hole/decidable_mem_nat.def(6)"decidable_mem_nat/a n l) // 
+#H4 @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 (|la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'greater than'" href="cic:/fakeuri.def(1)">/a n))
   [>H1 // 
-  |@le_to_not_lt @length_unique_le //
-   #x #memx cases(le_to_or_lt_eq … (H3 x memx)) //
-   #Heq @not_le_to_lt @(not_to_not … H4) #_ <Heq //
+  |@a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a @a href="cic:/matita/arithmetics/pidgeon_hole/length_unique_le.def(9)"length_unique_le/a //
+   #x #memx cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … (H3 x memx)) //
+   #Heq @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 … H4) #_ <Heq //
   ]
 qed.
 
-lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l  → 
-  (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
+img class="anchor" src="icons/tick.png" id="eq_length_to_mem_all"lemma eq_length_to_mem_all: ∀n,l. |la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n → a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l  → 
+  (∀x. x a title="list membership" href="cic:/fakeuri.def(1)"∈/a l → x a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n) → ∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → i a title="list membership" href="cic:/fakeuri.def(1)"∈/a l.
 #n elim n
-  [#l #_ #_ #_ #i #lti0 @False_ind @(absurd ? lti0 (not_le_Sn_O ?))
-  |#m #Hind #l #H #H1 #H2 #i #lei cases (le_to_or_lt_eq … lei)
-    [#leim @(mem_filter… (λi.¬(eqb m i))) 
-     cases (filter_eqb m … H1)
-      [2: * #H @False_ind @(absurd ?? H) @eq_length_to_mem //
-       #x #memx @le_S_S_to_le @H2 //]
+  [#l #_ #_ #_ #i #lti0 @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 ? lti0 (a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a ?))
+  |#m #Hind #l #H #H1 #H2 #i #lei cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lei)
+    [#leim @(a href="cic:/matita/basics/lists/search/mem_filter.def(3)"mem_filter/a… (λi.a title="boolean not" href="cic:/fakeuri.def(1)"¬/a(a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m i))) 
+     cases (a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"filter_eqb/a m … H1)
+      [2: * #H @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 ?? H) @a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"eq_length_to_mem/a //
+       #x #memx @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H2 //]
       * #memm #Hfilter @Hind
-        [@injective_S <H <(filter_length2 ? (eqb m) l) >Hfilter %
-        |@unique_filter @H1
-        |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3
-          [@le_S_S_to_le @H3
-          |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
-           @injective_notb >(mem_filter_true ???? memx) %
+        [@a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a <H <(a href="cic:/matita/basics/lists/search/filter_length2.def(5)"filter_length2/a ? (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m) l) >Hfilter %
+        |@a href="cic:/matita/basics/lists/search/unique_filter.def(4)"unique_filter/a @H1
+        |#x #memx cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … (H2 x (a href="cic:/matita/basics/lists/search/mem_filter.def(3)"mem_filter/a … memx))) #H3
+          [@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H3
+          |@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 (ma title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax)) [@a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a //] @a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"eqb_false_to_not_eq/a
+           @a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a >(a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"mem_filter_true/a ???? memx) %
           ]
-      |@le_S_S_to_le @leim
+      |@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @leim
       ]
-    |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //]
+    |#eqi @a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"eq_length_to_mem/a >eqi [@H |@H1 |#x #Hx @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a >eqi @H2 //]
     ]
   ]
 qed. 
 
-lemma lt_length_to_not_mem: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| < n →
-∃i. i < n ∧ ¬ (i ∈ l). 
+img class="anchor" src="icons/tick.png" id="lt_length_to_not_mem"lemma lt_length_to_not_mem: ∀n,l. a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l  → (∀x. x a title="list membership" href="cic:/fakeuri.def(1)"∈/a l → x a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n) → |la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n →
+a title="exists" href="cic:/fakeuri.def(1)"∃/ai. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a (i a title="list membership" href="cic:/fakeuri.def(1)"∈/a l). 
 #n elim n
-  [#l #_ #_ #H @False_ind /2/
-  |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni)
+  [#l #_ #_ #H @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/
+  |#m #Hind #l #Huni #Hmem #Hlen cases (a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"filter_eqb/a m … Huni)
     [2: * #H #_ %{m} % //
-    |* #memm #Hfilter cases (Hind (filter ? (λx. ¬(eqb m x)) l) ? ? ?)
-      [#i * #ltim #memi %{i} % [@le_S // ]
-       @(not_to_not … memi) @mem_filter_l @injective_notb >notb_notb
-       @not_eq_to_eqb_false @sym_not_eq @lt_to_not_eq //
-      |@unique_filter //
-      |#x #memx cases (le_to_or_lt_eq … (Hmem x ?))
-        [#H @le_S_S_to_le @H
-        |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
-         @injective_notb >(mem_filter_true ???? memx) %
-        |@(mem_filter … memx)
+    |* #memm #Hfilter cases (Hind (a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a ? (λx. a title="boolean not" href="cic:/fakeuri.def(1)"¬/a(a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m x)) l) ? ? ?)
+      [#i * #ltim #memi %{i} % [@a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a // ]
+       @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … memi) @a href="cic:/matita/basics/lists/search/mem_filter_l.def(4)"mem_filter_l/a @a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a >a href="cic:/matita/basics/bool/notb_notb.def(2)"notb_notb/a
+       @a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"not_eq_to_eqb_false/a @a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a @a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a //
+      |@a href="cic:/matita/basics/lists/search/unique_filter.def(4)"unique_filter/a //
+      |#x #memx cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … (Hmem x ?))
+        [#H @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H
+        |#H @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 (ma title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax)) [@a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a //] @a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"eqb_false_to_not_eq/a
+         @a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a >(a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"mem_filter_true/a ???? memx) %
+        |@(a href="cic:/matita/basics/lists/search/mem_filter.def(3)"mem_filter/a … memx)
         ]
-      |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H
-       @le_S_S_to_le @H
+      |<(a href="cic:/matita/basics/lists/search/filter_length2.def(5)"filter_length2/a … (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m)) in Hlen; >Hfilter #H
+       @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H
       ]
     ]
   ]
diff --git a/weblib/basics/append.ma b/weblib/basics/append.ma
deleted file mode 100644
index 5fe5dcee7..000000000
--- a/weblib/basics/append.ma
+++ /dev/null
@@ -1 +0,0 @@
-(* new script *)
\ No newline at end of file
-- 
2.39.2