From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 16 Dec 2010 11:54:35 +0000 (+0000)
Subject: New version of the library. Several files still do not compile.
X-Git-Tag: make_still_working~2648
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

New version of the library. Several files still do not compile.
---

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 69a9ff20b..3211814db 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -265,7 +265,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
   ]
 qed.
 
-(* Sigma e Pi - da generalizzare *)
+(* Sigma e Pi *)
 notation "Σ_{ ident i < n | p } f"
   with precedence 80
 for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}.
diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
new file mode 100644
index 000000000..414b71a15
--- /dev/null
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -0,0 +1,245 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/bigops.ma".
+include "arithmetics/primes.ma".
+
+(* binomial coefficient *)
+definition bc ≝ λn,k. n!/(k!*(n-k)!).
+
+lemma bceq :∀n,k. bc n k = n!/(k!*(n-k)!).
+// qed.
+
+theorem bc_n_n: ∀n. bc n n = 1.
+#n >bceq <minus_n_n <times_n_1 @div_n_n //
+qed.
+
+theorem bc_n_O: ∀n. bc n O = 1.
+#n >bceq <minus_n_O /2/
+qed.
+
+theorem fact_minus: ∀n,k. k < n → 
+  (n-k)*(n - S k)! = (n - k)!.
+#n #k (cases n)
+  [#ltO @False_ind /2/
+  |#l #ltl >minus_Sn_m [>commutative_times //|@le_S_S_to_le //]
+  ]
+qed.
+
+theorem bc2 : ∀n.
+∀k. k ≤n → k!*(n-k)! ∣ n!.
+#n (elim n) 
+  [#k #lek0 <(le_n_O_to_eq ? lek0) //
+  |#m #Hind #k generalize in match H1;cases k
+     [intro;simplify in ⊢ (? (? ? (? %)) ?);simplify in ⊢ (? (? % ?) ?);
+      rewrite > sym_times;rewrite < times_n_SO;apply reflexive_divides
+     |intro;elim (decidable_eq_nat n2 n1)
+        [rewrite > H3;rewrite < minus_n_n;
+         rewrite > times_n_SO in ⊢ (? ? %);apply reflexive_divides
+        |lapply (H n2)
+           [lapply (H (n1 - (S n2)))
+              [change in ⊢ (? ? %) with ((S n1)*n1!);
+               rewrite > (plus_minus_m_m n1 n2) in ⊢ (? ? (? (? %) ?))
+                 [rewrite > sym_plus;
+                  change in ⊢ (? ? (? % ?)) with ((S n2) + (n1 - n2));
+                  rewrite > sym_times in \vdash (? ? %);
+                  rewrite > distr_times_plus in ⊢ (? ? %);
+                  simplify in ⊢ (? (? ? (? %)) ?);
+                  apply divides_plus
+                    [rewrite > sym_times;
+                     change in ⊢ (? (? ? %) ?) with ((S n2)*n2!);
+                     rewrite > sym_times in ⊢ (? (? ? %) ?);
+                     rewrite < assoc_times;
+                     apply divides_times
+                       [rewrite > sym_times;assumption
+                       |apply reflexive_divides]
+                    |rewrite < fact_minus in ⊢ (? (? ? %) ?)
+                       [rewrite > sym_times in ⊢ (? (? ? %) ?);
+                        rewrite < assoc_times;
+                        apply divides_times
+                          [rewrite < eq_plus_minus_minus_minus in Hletin1;
+                             [rewrite > sym_times;rewrite < minus_n_n in Hletin1;
+                              rewrite < plus_n_O in Hletin1;assumption
+                             |lapply (le_S_S_to_le ? ? H2);
+                              elim (le_to_or_lt_eq ? ? Hletin2);
+                                [assumption
+                                |elim (H3 H4)]
+                             |constructor 1]
+                          |apply reflexive_divides]
+                       |lapply (le_S_S_to_le ? ? H2);
+                        elim (le_to_or_lt_eq ? ? Hletin2);
+                          [assumption
+                          |elim (H3 H4)]]]
+                 |apply le_S_S_to_le;assumption]
+              |apply le_minus_m;apply le_S_S_to_le;assumption]
+           |apply le_S_S_to_le;assumption]]]]
+qed.                      
+    
+theorem bc1: \forall n.\forall k. k < n \to bc (S n) (S k) = (bc n k) + (bc n (S k)). 
+intros.unfold bc.
+rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
+  [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)). 
+   rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
+   rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
+    [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
+     rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
+     rewrite > fact_minus
+      [rewrite < eq_div_plus
+        [rewrite < distr_times_plus.
+         simplify in ⊢ (? ? ? (? (? ? %) ?)).
+         rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
+         rewrite < plus_minus_m_m
+          [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+           reflexivity
+          |apply lt_to_le.
+           assumption
+          ]
+        |rewrite > (times_n_O O).
+         apply lt_times;apply lt_O_fact
+        |change in ⊢ (? (? % ?) ?) with ((S k)*k!);
+         rewrite < sym_times in ⊢ (? ? %);
+         rewrite > assoc_times;apply divides_times
+           [apply reflexive_divides
+           |apply bc2;apply le_S_S_to_le;constructor 2;assumption]
+        |rewrite < fact_minus
+           [rewrite > sym_times in ⊢ (? (? ? %) ?);rewrite < assoc_times;
+            apply divides_times
+              [apply bc2;assumption
+              |apply reflexive_divides]
+           |assumption]]
+     |assumption]
+  |apply lt_to_lt_O_minus;assumption
+  |rewrite > (times_n_O O).
+   apply lt_times;apply lt_O_fact]
+|apply lt_O_S
+|rewrite > (times_n_O O).
+ apply lt_times;apply lt_O_fact]
+qed.
+
+theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m.
+intro.elim n
+  [apply (le_n_O_elim ? H).
+   simplify.apply le_n
+  |elim (le_to_or_lt_eq ? ? H1)
+    [generalize in match H2.cases m;intro
+      [rewrite > bc_n_O.apply le_n
+      |rewrite > bc1
+        [apply (trans_le ? (bc n1 n2))
+          [apply H.apply le_S_S_to_le.apply lt_to_le.assumption
+          |apply le_plus_n_r
+          ]
+        |apply le_S_S_to_le.assumption
+        ]
+      ]
+    |rewrite > H2.
+     rewrite > bc_n_n.
+     apply le_n
+    ]
+  ]
+qed.
+
+theorem exp_plus_sigma_p:\forall a,b,n.
+exp (a+b) n = sigma_p (S n) (\lambda k.true) 
+  (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
+intros.elim n
+  [simplify.reflexivity
+  |simplify in ⊢ (? ? % ?).
+   rewrite > true_to_sigma_p_Sn
+    [rewrite > H;rewrite > sym_times in ⊢ (? ? % ?);
+     rewrite > distr_times_plus in ⊢ (? ? % ?);
+     rewrite < minus_n_n in ⊢ (? ? ? (? (? (? ? (? ? %)) ?) ?));
+     rewrite > sym_times in ⊢ (? ? (? % ?) ?);
+     rewrite > sym_times in ⊢ (? ? (? ? %) ?);
+     rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? % ?) ?);
+     rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? ? %) ?);
+     rewrite > true_to_sigma_p_Sn in ⊢ (? ? (? ? %) ?)
+       [rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
+        rewrite > assoc_plus;
+        apply eq_f2
+          [rewrite > sym_times;rewrite > assoc_times;autobatch paramodulation
+          |rewrite > (sigma_p_gi ? ? O);
+            [rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in ⊢ (? ? (? (? ? %) ?) ?)
+               [rewrite > (sigma_p_gi ? ? O) in ⊢ (? ? ? %);
+                  [rewrite > assoc_plus;apply eq_f2
+                     [autobatch paramodulation; 
+                     |rewrite < sigma_p_plus_1;
+                      rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in \vdash (? ? ? %);
+                        [apply eq_sigma_p
+                           [intros;reflexivity
+                           |intros;rewrite > sym_times;rewrite > assoc_times;
+                            rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
+                            rewrite > assoc_times;rewrite < assoc_times in ⊢ (? ? (? (? ? %) ?) ?);
+                            rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
+                            change in ⊢ (? ? (? (? ? (? % ?)) ?) ?) with (exp a (S (n1 - S x)));
+                            rewrite < (minus_Sn_m ? ? H1);rewrite > minus_S_S;
+                            rewrite > sym_times in \vdash (? ? (? ? %) ?);
+                            rewrite > assoc_times; 
+                            rewrite > sym_times in ⊢ (? ? (? ? (? ? %)) ?);
+                            change in \vdash (? ? (? ? (? ? %)) ?) with (exp b (S x));
+                            rewrite > assoc_times in \vdash (? ? (? ? %) ?);
+                            rewrite > sym_times in \vdash (? ? (? % ?) ?);
+                            rewrite > sym_times in \vdash (? ? (? ? %) ?);
+                            rewrite > assoc_times in \vdash (? ? ? %);
+                            rewrite > sym_times in \vdash (? ? ? %);
+                            rewrite < distr_times_plus;
+                            rewrite > sym_plus;rewrite < bc1;
+                              [reflexivity|assumption]]
+                        |intros;simplify;reflexivity
+                        |intros;simplify;reflexivity
+                        |intros;apply le_S_S;assumption
+                        |intros;reflexivity
+                        |intros 2;elim j
+                            [simplify in H2;destruct H2
+                            |simplify;reflexivity]
+                        |intro;elim j
+                            [simplify in H2;destruct H2
+                            |simplify;apply le_S_S_to_le;assumption]]]
+                  |apply le_S_S;apply le_O_n
+                  |reflexivity]
+               |intros;simplify;reflexivity
+               |intros;simplify;reflexivity
+               |intros;apply le_S_S;assumption
+               |intros;reflexivity
+               |intros 2;elim j
+                  [simplify in H2;destruct H2
+                  |simplify;reflexivity]
+               |intro;elim j
+                  [simplify in H2;destruct H2
+                  |simplify;apply le_S_S_to_le;assumption]]
+            |apply le_S_S;apply le_O_n
+            |reflexivity]]
+      |reflexivity]
+   |reflexivity]]
+qed.
+
+theorem exp_S_sigma_p:\forall a,n.
+exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
+intros.
+rewrite > plus_n_SO.
+rewrite > exp_plus_sigma_p.
+apply eq_sigma_p;intros
+  [reflexivity
+  |rewrite < exp_SO_n.
+   rewrite < times_n_SO.
+   reflexivity
+  ]
+qed.
+
+theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
+intros.simplify.
+rewrite < times_n_SO.
+rewrite < plus_n_O.
+rewrite < sym_times.simplify.
+rewrite < assoc_plus.
+rewrite < sym_plus.
+reflexivity.
+qed.
+
diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
new file mode 100644
index 000000000..e8f8a7732
--- /dev/null
+++ b/matita/matita/lib/arithmetics/congruence.ma
@@ -0,0 +1,118 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/primes.ma".
+
+(* successor mod n *)
+definition S_mod: nat → nat → nat ≝
+λn,m:nat. (S m) \mod n.
+
+definition congruent: nat → nat → nat → Prop ≝
+λn,m,p:nat. mod n p = mod m p.
+
+interpretation "congruent" 'congruent n m p = (congruent n m p).
+
+notation "hvbox(n break ≅_{p} m)"
+  non associative with precedence 45
+  for @{ 'congruent $n $m $p }.
+  
+theorem congruent_n_n: ∀n,p:nat.n ≅_{p} n .
+// qed.
+
+theorem transitive_congruent: 
+  ∀p.transitive nat (λn,m.congruent n m p).
+/2/ qed.
+
+theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
+#n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
+% // @lt_mod_m_m @(ltn_to_ltO … ltnm) 
+qed.
+
+theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
+#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?) 
+>(eq_div_O ? p) // @lt_mod_m_m //
+qed.
+
+theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m → 
+  n \mod p = (n \mod (m*p)) \mod p.
+#n #m #p #posp #posm
+@(div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
+(n/(m*p)*m + (n \mod (m*p)/p))) 
+  [@div_mod_spec_div_mod //
+  |% [@lt_mod_m_m //] >distributive_times_plus_r
+   >associative_plus <div_mod >associative_times <div_mod //
+  ]
+qed.
+
+theorem congruent_n_mod_n : ∀n,p:nat. O < p →
+ n ≅_{p} (n \mod p).
+/2/ qed.
+
+theorem congruent_n_mod_times : ∀n,m,p:nat. O < p → O < m → 
+  n ≅_{p} (n \mod (m*p)).
+/2/ qed.
+
+theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. O< p → 
+  n = r*p+m → n ≅_{p} m .
+#n #m #p #r #posp #eqn
+@(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
+  [@div_mod_spec_div_mod //
+  |% [@lt_mod_m_m //] >distributive_times_plus_r
+   >associative_plus <div_mod //
+  ]
+qed.
+
+theorem divides_to_congruent: ∀n,m,p:nat. O < p → m ≤ n → 
+  p ∣(n - m) → n ≅_{p} m .
+#n #m #p #posp #lemn * #l #eqpl 
+@(eq_times_plus_to_congruent … l posp) /2/
+qed.
+
+theorem congruent_to_divides: ∀n,m,p:nat.O < p → 
+  n ≅_{p} m → p ∣ (n - m).
+#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
+>commutative_times >(div_mod n p) in ⊢ (??%?)
+>(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
+<congnm <(minus_minus ? (n \mod p)) <minus_plus_m_m //
+qed.
+
+theorem mod_times: ∀n,m,p:nat. O < p → 
+  n*m ≅_{p} (n \mod p)*(m \mod p).
+#n #m #p #posp @(eq_times_plus_to_congruent ?? p 
+  ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
+@(trans_eq ?? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
+  [@eq_f2 //
+  |@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
+    (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))) //
+   >distributive_times_plus >distributive_times_plus_r 
+   >distributive_times_plus_r <associative_plus @eq_f2 //
+  ]
+qed.
+
+theorem congruent_times: ∀n,m,n1,m1,p. O < p → 
+  n ≅_{p} n1 → m ≅_{p} m1 → n*m ≅_{p} n1*m1 .
+#n #m #n1 #m1 #p #posp #congn #congm
+@(transitive_congruent … (mod_times n m p posp))
+>congn >congm @sym_eq @mod_times //
+qed.
+
+(*
+theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
+congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
+intros.
+elim n. simplify.
+apply congruent_n_mod_n.assumption.
+simplify.
+apply congruent_times.
+assumption.
+apply congruent_n_mod_n.assumption.
+assumption.
+qed. *)
diff --git a/matita/matita/lib/arithmetics/div_and_mod.ma b/matita/matita/lib/arithmetics/div_and_mod.ma
index f2b0849af..cf19b8203 100644
--- a/matita/matita/lib/arithmetics/div_and_mod.ma
+++ b/matita/matita/lib/arithmetics/div_and_mod.ma
@@ -136,7 +136,6 @@ theorem div_times: ∀a,b:nat. O < b → a*b/b = a.
 @(div_mod_spec_to_eq (a*b) b … O (div_mod_spec_div_mod …))
 // @div_mod_spec_intro // qed.
 
-(*
 theorem div_n_n: ∀n:nat. O < n → n / n = 1.
 /2/ qed.
 
@@ -148,7 +147,7 @@ theorem eq_div_O: ∀n,m. n < m → n / m = O.
 theorem mod_n_n: ∀n:nat. O < n → n \mod n = O.
 #n #posn 
 @(div_mod_spec_to_eq2 n n … 1 0 (div_mod_spec_div_mod …))
-/2/ qed. *)
+/2/ qed. 
 
 theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m → 
 ((S n) \mod m) = S (n \mod m).
@@ -407,7 +406,7 @@ O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b).
 @(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
   [>(div_times_times … posc) // @div_mod_spec_div_mod /2/
   |@div_mod_spec_intro
-    [(applyS monotonic_lt_times_l) /2/
+    [applyS (monotonic_lt_times_r … c posc) /2/
     |(applyS (eq_f …(λx.x*c))) //
     ]
   ]
diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index 1c7adf69b..1205044be 100644
--- a/matita/matita/lib/arithmetics/exp.ma
+++ b/matita/matita/lib/arithmetics/exp.ma
@@ -75,11 +75,10 @@ qed.
 
 theorem le_exp: ∀n,m,p:nat. O < p →
   n ≤m → p^n ≤ p^m.
-@nat_elim2 
-  [#n #m #ltm #len @lt_O_exp //
-  |#n #m #_ #len @False_ind /2/
-  |#n #m #Hind #p #posp #lenm normalize @le_times //
-   @Hind /2/
+@nat_elim2 #n #m
+  [#ltm #len @lt_O_exp //
+  |#_ #len @False_ind /2/
+  |#Hind #p #posp #lenm normalize @le_times // @Hind /2/
   ]
 qed.
 
diff --git a/matita/matita/lib/arithmetics/gcd.ma b/matita/matita/lib/arithmetics/gcd.ma
new file mode 100644
index 000000000..86b0600be
--- /dev/null
+++ b/matita/matita/lib/arithmetics/gcd.ma
@@ -0,0 +1,406 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/primes.ma".
+  
+let rec gcd_aux p m n: nat ≝
+match p with 
+  [O ⇒ m
+  |S q ⇒ 
+    match dividesb n m with
+    [ true ⇒ n
+    | false ⇒ gcd_aux q n (m \mod n)]].
+    
+definition gcd : nat → nat → nat ≝ λn,m:nat.
+  match leb n m with
+  [ true ⇒ gcd_aux n m n 
+  | false ⇒ gcd_aux m n m ].
+  
+theorem commutative_gcd: ∀n,m. gcd n m = gcd m n.
+#n #m normalize @leb_elim 
+  [#lenm cases(le_to_or_lt_eq … lenm)
+    [#ltnm >not_le_to_leb_false // @lt_to_not_le //
+    |#eqnm >eqnm (cases (leb m m)) //
+    ]
+  |#notlenm >le_to_leb_true // @(transitive_le ? (S m)) //
+   @not_le_to_lt //
+  ]
+qed.
+
+theorem gcd_O_l: ∀m. gcd O m = m. 
+// qed.  
+  
+theorem divides_mod: ∀p,m,n:nat. O < n → 
+  p ∣ m → p ∣ n → p ∣ (m \mod n).
+#p #m #n #posn * #qm #eqm * #qn #eqn
+@(quotient ?? (qm - qn*(m / n))) >distributive_times_minus
+<eqm <associative_times <eqn @sym_eq @plus_to_minus /2/
+qed.
+
+theorem divides_mod_to_divides: ∀p,m,n:nat. O < n →
+  p ∣ (m \mod n) → p ∣ n → p ∣ m.
+#p #m #n #posn * #q1 #eq1 * #q2 #eq2
+@(quotient p m ((q2*(m / n))+q1)) >distributive_times_plus
+<eq1 <associative_times <eq2 /2/
+qed.
+
+lemma divides_to_gcd_aux: ∀p,m,n. O < p → O < n →n ∣ m → 
+  gcd_aux p m n = n.
+#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm normalize 
+>divides_to_dividesb_true normalize //
+qed.
+
+theorem divides_to_gcd: ∀m,n. O < n → n ∣ m → 
+  gcd n m = n.
+#m #n #posn (cases m)
+ [>commutative_gcd //
+ |#l #divn (cut (n ≤ (S l))) [@divides_to_le //] #len normalize
+  >le_to_leb_true // normalize @divides_to_gcd_aux //
+ ]
+qed.
+
+lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m → 
+  gcd_aux (S p) m n = gcd_aux p n (m \mod n).
+#p #m #n #lenm #divnm normalize >not_divides_to_dividesb_false
+normalize // qed.
+
+theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p →
+  gcd_aux p m n ∣ m ∧ gcd_aux p m n ∣ n. 
+#p (elim p)
+  [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/
+  |#q #Hind #m #n #posn #lenm #lenS cases(decidable_divides n m)
+    [#divnm >(divides_to_gcd_aux … posn divnm) // % //
+    |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
+     cut (gcd_aux q n (m \mod n) ∣ n ∧
+          gcd_aux q n (m \mod n) ∣ mod m n)
+      [cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
+       @Hind
+        [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
+         @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
+        |/2/
+        |@le_S_S_to_le @(transitive_le … ltmod lenS)
+        ]
+      |* #H #H1 % [@(divides_mod_to_divides … posn H1) // |//]
+      ]
+    ]
+  ]
+qed.
+
+theorem divides_gcd_nm: ∀n,m.
+  gcd n m ∣ m ∧ gcd n m ∣ n.
+#n #m cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO <eqnO /2/]
+#posn cases(le_to_or_lt_eq …(le_O_n m)) [|#eqmO <eqmO /2/]
+#posm normalize @leb_elim normalize  
+  [#lenm @divides_gcd_aux_mn //
+  |#notlt normalize cut (∀A,B. A∧B → B∧A) [#A #B * /2/] #sym_and
+   @sym_and @divides_gcd_aux_mn // @(transitive_le ? (S m)) //
+   @not_le_to_lt //
+  ]
+qed. 
+
+theorem divides_gcd_l: ∀n,m. gcd n m ∣ n.
+#n #m @(proj2  ? ? (divides_gcd_nm n m)).
+qed.
+
+theorem divides_gcd_r: \forall n,m. gcd n m ∣ m.
+#n #m @(proj1 ? ? (divides_gcd_nm n m)).
+qed.
+
+theorem divides_times_gcd_aux: ∀p,m,n,d,c. 
+  O < c → O < n → n ≤ m → n ≤ p →
+    d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd_aux p m n. 
+#p (elim p) 
+  [#m #n #d #c #_ #posn #_ #lenO @False_ind @(absurd … lenO) /2/
+  |#q #Hind #m #n #d #c #posc #posn #lenm #lenS #dcm #dcn
+   cases(decidable_divides n m)
+    [#divnm >(divides_to_gcd_aux … posn divnm) //
+    |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
+     cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
+     @Hind //
+      [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
+       @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
+      |/2/
+      |@le_S_S_to_le @(transitive_le … ltmod lenS)
+      |<times_mod // < (commutative_times c m)
+       <(commutative_times c n) @divides_mod //
+       >(times_n_O 0) @lt_times //
+      ]
+    ]
+  ]
+qed. 
+
+(*a particular case of the previous theorem, with c=1 *)
+theorem divides_gcd_aux: ∀p,m,n,d. O < n → n ≤ m → n ≤ p →
+  d ∣ m \to d ∣ n \to d ∣ gcd_aux p m n.
+  (* bell'esempio di smart application *)
+/2/ qed. 
+
+theorem divides_d_times_gcd: ∀m,n,d,c. O < c → 
+  d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd n m. 
+#m #n #d #c #posc #dcm #dcn 
+cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO <eqnO @dcm] #posn 
+cases(le_to_or_lt_eq …(le_O_n m)) [|#eqmO <eqmO <commutative_gcd @dcn] #posm
+normalize @leb_elim normalize
+  [#lenm @divides_times_gcd_aux //
+  |#nlenm @divides_times_gcd_aux //
+   @(transitive_le ? (S m)) // @not_le_to_lt //
+  ]
+qed.
+
+(* a particular case of the previous theorem, with c=1 *)
+theorem divides_d_gcd: ∀m,n,d. 
+ d ∣ m → d ∣ n → d ∣ gcd n m. 
+/2/ (* bello *)
+qed.
+
+theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m →  n ≤ p →
+  ∃a,b. a*n - b*m = gcd_aux p m n ∨ b*m - a*n = gcd_aux p m n.
+#p (elim p)
+  [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/
+  |#q #Hind #m #n #posn #lenm #lenS 
+   cut (0 < m) [@lt_to_le_to_lt //] #posm 
+   cases(decidable_divides n m)
+    [#divnm >(divides_to_gcd_aux … posn divnm) // 
+     @(ex_intro ?? 1) @(ex_intro ?? 0) %1 //
+    |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
+     cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
+     lapply (Hind n (m \mod n) ???)
+      [@le_S_S_to_le @(transitive_le … ltmod lenS)
+      |/2/
+      |cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
+       @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
+      ]
+     * #a * #b * #H
+      [(* first case *)
+       <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %2
+       <commutative_plus >distributive_times_plus_r 
+       >(div_mod m n) in ⊢(? ? (? % ?) ?)
+       >associative_times <commutative_plus >distributive_times_plus
+       <minus_minus <commutative_plus <plus_minus //
+      |(* second case *)
+        <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
+        >distributive_times_plus_r
+        >(div_mod m n) in ⊢ (? ? (? ? %) ?)
+        >distributive_times_plus >associative_times
+        <minus_minus <commutative_plus <plus_minus //
+      ]
+    ]
+  ]
+qed.
+
+theorem eq_minus_gcd:
+  ∀m,n.∃ a,b.a*n - b*m = gcd n m ∨ b*m - a*n = gcd n m.
+  #m #n cases(le_to_or_lt_eq …(le_O_n n)) 
+  [|#eqn0 >eqn0 @(ex_intro ?? O) @(ex_intro ? ? 1) %2 applyS minus_n_O]
+#posn cases(le_to_or_lt_eq …(le_O_n m)) 
+  [|#eqm0 >eqm0 @(ex_intro ?? 1) @(ex_intro ? ? 0) %1 applyS minus_n_O]
+#posm normalize @leb_elim normalize
+  [#lenm @eq_minus_gcd_aux //
+  |#nlenm lapply(eq_minus_gcd_aux m n m posm ? (le_n m))
+    [@(transitive_le … (not_le_to_lt … nlenm)) //]
+   * #a * #b * #H @(ex_intro ?? b) @(ex_intro ?? a) [%2 // |%1 //]
+  ]
+qed.
+
+(* some properties of gcd *)
+
+theorem gcd_O_to_eq_O:∀m,n:nat. 
+  gcd m n = O → m = O ∧ n = O.
+#m #n #H cut (O ∣ n ∧ O ∣ m)
+  [<H @divides_gcd_nm| * * #q1 #H1 * #q2 #H2 % // ]
+qed.
+
+theorem lt_O_gcd:∀m,n:nat. O < n → O < gcd m n.
+#m #n #posn @(nat_case (gcd m n)) // 
+#H (cases (gcd_O_to_eq_O m n H)) //
+qed.
+
+theorem gcd_n_n: ∀n.gcd n n = n.
+#n (cases n) //
+#m @le_to_le_to_eq
+  [@divides_to_le //
+  |@divides_to_le (*/2/*) [@lt_O_gcd // |@divides_d_gcd // ]
+  ]
+qed.
+
+(* some properties or relative primes - i.e. gcd = 1 *)
+theorem gcd_1_to_lt_O: ∀i,n. 1 < n → gcd i n = 1 → O < i.
+#i #n #lt1n #gcd1 cases (le_to_or_lt_eq ?? (le_O_n i)) //
+#iO @False_ind @(absurd … gcd1) <iO normalize
+@sym_not_eq @lt_to_not_eq //
+qed.
+
+theorem gcd_1_to_lt_n: ∀i,n. 1 < n → 
+  i ≤ n → gcd i n = 1 → i < n.
+#i #n #lt1n #lein #gcd1 cases (le_to_or_lt_eq ?? lein) //
+(* impressive *)
+qed.
+
+theorem  gcd_n_times_nm: ∀n,m. O < m → gcd n (n*m) = n.
+#n #m #posm @(nat_case n) //
+#l #eqn @le_to_le_to_eq
+  [@divides_to_le //
+  |@divides_to_le
+    [@lt_O_gcd >(times_n_O O) @lt_times // |@divides_d_gcd /2/]
+  ]
+qed.
+
+theorem le_gcd_times: ∀m,n,p. O< p → gcd m n ≤ gcd m (n*p).
+#m #n #p #posp @(nat_case n) // 
+#l #eqn @divides_to_le [@lt_O_gcd >(times_n_O O) @lt_times //] 
+@divides_d_gcd [@(transitive_divides ? (S l)) /2/ |//]
+qed.
+
+theorem gcd_times_SO_to_gcd_SO: ∀m,n,p:nat. O < n → O < p → 
+  gcd m (n*p) = 1 → gcd m n = 1.
+#m #n #p #posn #posp #gcd1 @le_to_le_to_eq
+  [<gcd1 @le_gcd_times // | @lt_O_gcd //]
+qed.
+
+(* for the "converse" of the previous result see the end  of this development *)
+
+theorem eq_gcd_SO_to_not_divides: ∀n,m. 1 < n → 
+  gcd n m = 1 → n ∤ m.
+#n #m #lt1n #gcd1 @(not_to_not … (gcd n m = n))
+  [#divnm @divides_to_gcd /2/ | /2/]
+qed.
+
+theorem gcd_SO_n: ∀n:nat. gcd 1 n = 1.
+#n @le_to_le_to_eq
+  [@divides_to_le // |>commutative_gcd @lt_O_gcd //]
+qed.
+
+theorem divides_gcd_mod: ∀m,n:nat. O < n →
+  gcd m n ∣ gcd n (m \mod n).
+#m #n #posn @divides_d_gcd [@divides_mod // | //]
+qed.
+
+theorem divides_mod_gcd: ∀m,n:nat. O < n →
+  gcd n (m \mod n) ∣ gcd m n.
+#m #n #posn @divides_d_gcd
+  [@divides_gcd_l |@(divides_mod_to_divides ?? n) //]
+qed.
+
+theorem gcd_mod: ∀m,n:nat. O < n →
+  gcd n (m \mod n) = gcd m n.
+#m #n #posn @antisymmetric_divides
+  [@divides_mod_gcd // | @divides_gcd_mod //]
+qed.
+
+(* gcd and primes *)
+
+theorem prime_to_gcd_1: ∀n,m:nat. prime n → n ∤ m →
+  gcd n m = 1.
+(* bella dimostrazione *)
+#n #m * #lt1n #primen #ndivnm @le_to_le_to_eq
+  [@not_lt_to_le @(not_to_not … (primen (gcd n m) (divides_gcd_l …)))
+   @(not_to_not ? (n ∣m)) //
+  |@lt_O_gcd @not_eq_to_le_to_lt // @(not_to_not ? (n ∣ m)) //
+  ]
+qed.
+
+(* primes and divides *)
+theorem divides_times_to_divides: ∀p,n,m:nat.prime p → 
+  p ∣ n*m → p ∣ n ∨ p ∣ m.
+#p #n #m #primp * #c #nm
+cases (decidable_divides p n) /2/ #ndivpn %2 
+cut (∃a,b. a*n - b*p = 1 ∨ b*p - a*n = 1)
+  [<(prime_to_gcd_1 … primp ndivpn) >commutative_gcd @eq_minus_gcd]
+* #a * #b * #H
+  [@(quotient ?? (a*c-b*m)) >distributive_times_minus <associative_times 
+   >(commutative_times p) >associative_times <nm <associative_times
+   <associative_times <commutative_times >(commutative_times (p*b))
+   <distributive_times_minus //
+  |@(quotient ?? (b*m -a*c)) >distributive_times_minus <(associative_times p)
+   <(associative_times p) <(commutative_times a) >(associative_times a)
+   <nm <(associative_times a) <commutative_times >(commutative_times (a*n))
+   <distributive_times_minus //
+  ]
+qed.
+
+theorem divides_exp_to_divides: 
+∀p,n,m:nat. prime p → p ∣n^m → p ∣ n.
+#p #n #m #primep (elim m) normalize /2/
+#l #Hind #H cases(divides_times_to_divides  … primep H) /2/
+qed.
+
+theorem divides_exp_to_eq: 
+∀p,q,m:nat. prime p → prime q →
+  p ∣ q^m → p = q.
+#p #q #m #H * #lt1q #primeq #H @primeq /2/
+qed.
+
+(* relative primes *)
+theorem eq_gcd_times_1: ∀p,n,m:nat. O < n → O < m →
+ gcd p n = 1 → gcd p m = 1 → gcd p (n*m) = 1.
+#p #n #m #posn #posm #primepn #primepm 
+@le_to_le_to_eq [|@lt_O_gcd >(times_n_O 0) @lt_times //]
+@not_lt_to_le % #lt1gcd
+cut (smallest_factor (gcd p (n*m)) ∣ n ∨ 
+     smallest_factor (gcd p (n*m)) ∣ m)
+  [@divides_times_to_divides
+    [@prime_smallest_factor_n //
+    |@(transitive_divides ? (gcd p (n*m))) // 
+     @divides_smallest_factor_n /2/
+    ]
+  |* #H
+    [@(absurd ?? (lt_to_not_le …(lt_SO_smallest_factor … lt1gcd)))
+     <primepn @divides_to_le // @divides_d_gcd //
+     @(transitive_divides … (divides_smallest_factor_n …))
+       [@lt_O_gcd >(times_n_O 0) @lt_times // | //]
+    |@(absurd ?? (lt_to_not_le … (lt_SO_smallest_factor …lt1gcd)))
+     <primepm @divides_to_le // @divides_d_gcd //
+     @(transitive_divides … (divides_smallest_factor_n …))
+       [@lt_O_gcd >(times_n_O 0) @lt_times // | //]
+  ]
+qed.
+
+
+theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
+gcd p n = 1 → p ∣ (n*m) → p ∣ m.
+#p #m #n #posn #gcd1 * #c #nm
+cases(eq_minus_gcd m p) #a * #b * #H >gcd1 in H #H 
+  [@(quotient ?? (a*n-c*b)) >distributive_times_minus <associative_times 
+   <associative_times <nm >(commutative_times m) >commutative_times
+   >associative_times <distributive_times_minus //
+  |@(quotient ?? (c*b-a*n)) >distributive_times_minus <associative_times 
+   <associative_times <nm >(commutative_times m) <(commutative_times n)
+   >associative_times <distributive_times_minus //
+  ]
+qed.
+
+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+  [elim H.apply False_ind.
+   apply H2.apply sym_eq.apply H8
+    [assumption
+    |apply prime_to_lt_SO.assumption
+    ]
+  |elim H6.
+   apply (witness ? ? n1).
+   rewrite > assoc_times.
+   rewrite < H7.assumption
+  ]
+qed.
+*)
+
+theorem divides_to_divides_times: ∀p,q,n. prime p  → p ∤ q →
+ p ∣ n → q ∣ n → p*q ∣ n.
+#p #q #n #primep #notdivpq #divpn * #b #eqn (>eqn in divpn)
+#divpn cases(divides_times_to_divides ??? primep divpn) #H
+  [@False_ind /2/ 
+  |cases H #c #eqb @(quotient ?? c) >eqb <associative_times //
+  ]
+qed.
\ No newline at end of file
diff --git a/matita/matita/lib/arithmetics/log.ma b/matita/matita/lib/arithmetics/log.ma
new file mode 100644
index 000000000..b48aea3f8
--- /dev/null
+++ b/matita/matita/lib/arithmetics/log.ma
@@ -0,0 +1,474 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*
+include "datatypes/constructors.ma".
+include "nat/minimization.ma".
+include "nat/relevant_equations.ma".
+include "nat/primes.ma".
+include "nat/iteration2.ma".
+include "nat/div_and_mod_diseq.ma".
+
+definition log \def \lambda p,n.
+max n (\lambda x.leb (exp p x) n).
+
+theorem le_exp_log: \forall p,n. O < n \to
+exp p (log p n) \le n.
+intros.
+apply leb_true_to_le.
+unfold log.
+apply (f_max_true (\lambda x.leb (exp p x) n)).
+apply (ex_intro ? ? O).
+split
+  [apply le_O_n
+  |apply le_to_leb_true.simplify.assumption
+  ]
+qed.
+
+theorem log_SO: \forall n. S O < n \to log n (S O) = O.
+intros.
+apply sym_eq.apply le_n_O_to_eq.
+apply (le_exp_to_le n)
+  [assumption
+  |simplify in ⊢ (? ? %).
+   apply le_exp_log.
+   apply le_n
+  ]
+qed.
+
+theorem lt_to_log_O: \forall n,m. O < m \to m < n \to log n m = O.
+intros.
+apply sym_eq.apply le_n_O_to_eq.
+apply le_S_S_to_le.
+apply (lt_exp_to_lt n)
+  [apply (le_to_lt_to_lt ? m);assumption
+  |simplify in ⊢ (? ? %).
+   rewrite < times_n_SO.
+   apply (le_to_lt_to_lt ? m)
+    [apply le_exp_log.assumption
+    |assumption
+    ]
+  ]
+qed.
+
+theorem lt_log_n_n: \forall p, n. S O < p \to O < n \to log p n < n.
+intros.
+cut (log p n \le n)
+  [elim (le_to_or_lt_eq ? ? Hcut)
+    [assumption
+    |absurd (exp p n \le n)
+      [rewrite < H2 in ⊢ (? (? ? %) ?).
+       apply le_exp_log.
+       assumption
+      |apply lt_to_not_le.
+       apply lt_m_exp_nm.
+       assumption
+      ]
+    ]
+  |unfold log.apply le_max_n
+  ]
+qed.
+
+theorem lt_O_log: \forall p,n. O < n \to p \le n \to O < log p n.
+intros.
+unfold log.
+apply not_lt_to_le.
+intro.
+apply (leb_false_to_not_le ? ? ? H1).
+rewrite > (exp_n_SO p).
+apply (lt_max_to_false ? ? ? H2).
+assumption.
+qed.
+
+theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n.
+intros.
+cases n
+  [apply le_n
+  |apply lt_to_le.
+   apply lt_log_n_n
+    [assumption|apply lt_O_S]
+  ]
+qed.
+
+theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)).
+intros.cases n
+  [simplify.rewrite < times_n_SO.apply lt_to_le.assumption
+  |apply not_le_to_lt.
+   apply leb_false_to_not_le.
+   apply (lt_max_to_false ? (S n1) (S (log p (S n1))))
+    [apply le_S_S.apply le_n
+    |apply lt_log_n_n
+      [assumption|apply lt_O_S]
+    ]
+  ]
+qed.
+
+theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to
+log p (n*m) \le S(log p n+log p m).
+intros.
+unfold in ⊢ (? (% ? ?) ?).
+apply f_false_to_le_max
+  [apply (ex_intro ? ? O).
+   split
+    [apply le_O_n
+    |apply le_to_leb_true.
+     simplify.
+     rewrite > times_n_SO.
+     apply le_times;assumption
+    ]
+  |intros.
+   apply lt_to_leb_false.
+   apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
+    [apply lt_times;apply lt_exp_log;assumption
+    |rewrite < exp_plus_times.
+     apply le_exp
+      [apply lt_to_le.assumption
+      |simplify.
+       rewrite < plus_n_Sm.
+       assumption
+      ]
+    ]
+  ]
+qed.
+  
+theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m).
+intros.
+cases n
+  [apply le_O_n
+  |cases m
+    [rewrite < times_n_O.
+     apply le_O_n
+    |apply log_times1
+      [assumption
+      |apply lt_O_S
+      |apply lt_O_S
+      ]
+    ]
+  ]
+qed.
+
+theorem log_times_l: \forall p,n,m.O < n \to O < m \to S O < p \to 
+log p n+log p m \le log p (n*m) .
+intros.
+unfold log in ⊢ (? ? (% ? ?)).
+apply f_m_to_le_max
+  [elim H
+    [rewrite > log_SO
+      [simplify.
+       rewrite < plus_n_O.
+       apply le_log_n_n.
+       assumption
+      |assumption
+      ]
+    |elim H1
+      [rewrite > log_SO
+        [rewrite < plus_n_O.
+         rewrite < times_n_SO.
+         apply le_log_n_n.
+         assumption
+        |assumption
+        ]
+      |apply (trans_le ? (S n1 + S n2))
+        [apply le_plus;apply le_log_n_n;assumption
+        |simplify.
+         apply le_S_S.
+         rewrite < plus_n_Sm.
+         change in ⊢ (? % ?) with ((S n1)+n2).
+         rewrite > sym_plus.
+         apply le_plus_r.
+         change with (n1 < n1*S n2).
+         rewrite > times_n_SO in ⊢ (? % ?).
+         apply lt_times_r1
+          [assumption
+          |apply le_S_S.assumption
+          ]
+        ]
+      ]
+    ]
+  |apply le_to_leb_true.
+   rewrite > exp_plus_times.
+   apply le_times;apply le_exp_log;assumption
+  ]
+qed.
+
+theorem log_exp: \forall p,n,m.S O < p \to O < m \to
+log p ((exp p n)*m)=n+log p m.
+intros.
+unfold log in ⊢ (? ? (% ? ?) ?).
+apply max_spec_to_max.
+unfold max_spec.
+split
+  [split
+    [elim n
+      [simplify.
+       rewrite < plus_n_O.
+       apply le_log_n_n.
+       assumption
+      |simplify.
+       rewrite > assoc_times.
+       apply (trans_le ? ((S(S O))*(p\sup n1*m)))
+        [apply le_S_times_SSO
+          [rewrite > (times_n_O O) in ⊢ (? % ?).
+           apply lt_times
+            [apply lt_O_exp.
+             apply lt_to_le.
+             assumption
+            |assumption
+            ]
+          |assumption
+          ]
+        |apply le_times
+          [assumption
+          |apply le_n
+          ]
+        ]
+      ]
+    |simplify.
+     apply le_to_leb_true.
+     rewrite > exp_plus_times.
+     apply le_times_r.
+     apply le_exp_log.
+     assumption
+    ]
+  |intros.
+   simplify.
+   apply lt_to_leb_false.
+   apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
+    [apply lt_times_r1
+      [apply lt_O_exp.apply lt_to_le.assumption
+      |apply lt_exp_log.assumption
+      ]
+    |rewrite < exp_plus_times.
+     apply le_exp
+      [apply lt_to_le.assumption
+      |rewrite < plus_n_Sm.
+       assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem eq_log_exp: \forall p,n.S O < p \to
+log p (exp p n)=n.
+intros.
+rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > log_exp
+  [rewrite > log_SO
+    [rewrite < plus_n_O.reflexivity
+    |assumption
+    ]
+  |assumption
+  |apply le_n
+  ]
+qed.
+
+theorem log_exp1: \forall p,n,m.S O < p \to
+log p (exp n m) \le m*S(log p n).
+intros.elim m
+  [simplify in ⊢ (? (? ? %) ?).
+   rewrite > log_SO
+    [apply le_O_n
+    |assumption
+    ]
+  |simplify.
+   apply (trans_le ? (S (log p n+log p (n\sup n1))))
+    [apply log_times.assumption
+    |apply le_S_S.
+     apply le_plus_r.
+     assumption
+    ]
+  ]
+qed.
+    
+theorem log_exp2: \forall p,n,m.S O < p \to O < n \to
+m*(log p n) \le log p (exp n m).
+intros.
+apply le_S_S_to_le.
+apply (lt_exp_to_lt p)
+  [assumption
+  |rewrite > sym_times.
+   rewrite < exp_exp_times.
+   apply (le_to_lt_to_lt ? (exp n m))
+    [elim m
+      [simplify.apply le_n
+      |simplify.apply le_times
+        [apply le_exp_log.
+         assumption
+        |assumption
+        ]
+      ]
+    |apply lt_exp_log.
+     assumption
+    ]
+  ]
+qed.
+
+lemma le_log_plus: \forall p,n.S O < p \to log p n \leq log p (S n).
+intros;apply (bool_elim ? (leb (p*(exp p n)) (S n)))
+  [simplify;intro;rewrite > H1;simplify;apply (trans_le ? n)
+    [apply le_log_n_n;assumption
+    |apply le_n_Sn]
+  |intro;unfold log;simplify;rewrite > H1;simplify;apply le_max_f_max_g;
+   intros;apply le_to_leb_true;constructor 2;apply leb_true_to_le;assumption]
+qed.
+
+theorem le_log: \forall p,n,m. S O < p \to n \le m \to 
+log p n \le log p m.
+intros.elim H1
+  [constructor 1
+  |apply (trans_le ? ? ? H3);apply le_log_plus;assumption]
+qed.
+         
+theorem log_div: \forall p,n,m. S O < p \to O < m \to m \le n \to
+log p (n/m) \le log p n -log p m.
+intros.
+apply le_plus_to_minus_r.
+apply (trans_le ? (log p ((n/m)*m)))
+  [apply log_times_l
+    [apply le_times_to_le_div
+      [assumption
+      |rewrite < times_n_SO.
+       assumption
+      ]
+    |assumption
+    |assumption
+    ]
+  |apply le_log
+    [assumption
+    |rewrite > (div_mod n m) in ⊢ (? ? %)
+      [apply le_plus_n_r
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem log_n_n: \forall n. S O < n \to log n n = S O.
+intros.
+rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > log_exp
+  [rewrite > log_SO
+    [reflexivity
+    |assumption
+    ]
+  |assumption
+  |apply le_n
+  ]
+qed.
+
+theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to
+log i ((S(S O))*n) = S O.
+intros.
+apply antisymmetric_le
+  [apply not_lt_to_le.intro.
+   apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O))))
+    [rewrite > exp_SSO.
+     apply lt_times
+      [apply (le_to_lt_to_lt ? n);assumption
+      |assumption
+      ]
+    |apply (trans_le ? (exp i (log i ((S(S O))*n))))
+      [apply le_exp
+        [apply (ltn_to_ltO ? ? H1)
+        |assumption
+        ]
+      |apply le_exp_log.
+       rewrite > (times_n_O O) in ⊢ (? % ?).
+       apply lt_times
+        [apply lt_O_S
+        |apply lt_to_le.assumption
+        ]
+      ]
+    ]
+  |apply (trans_le ? (log i i))
+    [rewrite < (log_n_n i) in ⊢ (? % ?)
+      [apply le_log
+        [apply (trans_lt ? n);assumption
+        |apply le_n
+        ]
+      |apply (trans_lt ? n);assumption
+      ]
+    |apply le_log
+      [apply (trans_lt ? n);assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem exp_n_O: \forall n. O < n \to exp O n = O.
+intros.apply (lt_O_n_elim ? H).intros.
+simplify.reflexivity.
+qed.
+
+(*
+theorem tech1: \forall n,i.O < n \to
+(exp (S n) (S(S i)))/(exp n (S i)) \le ((exp n i) + (exp (S n) (S i)))/(exp n i).
+intros.
+simplify in ⊢ (? (? ? %) ?).
+rewrite < eq_div_div_div_times
+  [apply monotonic_div
+    [apply lt_O_exp.assumption
+    |apply le_S_S_to_le.
+     apply lt_times_to_lt_div.
+     change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))).
+      
+      
+  |apply (trans_le ? ((n)\sup(i)*(S n)\sup(S i)/(n)\sup(S i)))
+    [apply le_times_div_div_times.
+     apply lt_O_exp.assumption
+    |apply le_times_to_le_div2
+      [apply lt_O_exp.assumption
+      |simplify.
+
+theorem tech1: \forall a,b,n,m.O < m \to
+n/m \le b \to (a*n)/m \le a*b.
+intros.
+apply le_times_to_le_div2
+  [assumption
+  |
+
+theorem tech2: \forall n,m. O < n \to 
+(exp (S n) m) / (exp n m) \le (n + m)/n.
+intros.
+elim m
+  [rewrite < plus_n_O.simplify.
+   rewrite > div_n_n.apply le_n
+  |apply le_times_to_le_div
+    [assumption
+    |apply (trans_le ? (n*(S n)\sup(S n1)/(n)\sup(S n1)))
+      [apply le_times_div_div_times.
+       apply lt_O_exp
+      |simplify in ⊢ (? (? ? %) ?).
+       rewrite > sym_times in ⊢ (? (? ? %) ?). 
+       rewrite < eq_div_div_div_times
+        [apply le_times_to_le_div2
+          [assumption
+          |
+      
+      
+theorem le_log_sigma_p:\forall n,m,p. O < m \to S O < p \to
+log p (exp n m) \le sigma_p n (\lambda i.true) (\lambda i. (m / i)).
+intros.
+elim n
+  [rewrite > exp_n_O
+    [simplify.apply le_n
+    |assumption
+    ]
+  |rewrite > true_to_sigma_p_Sn
+    [apply (trans_le ? (m/n1+(log p (exp n1 m))))
+      [
+*)
+*)
diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 33a75b67b..eda9d0166 100644
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -190,7 +190,7 @@ n ≤ m  → ∀b.min n b f ≤ min m b f.
   [#n #leSO @False_ind /2/ 
   |#n #m #Hind #leSS #b
    (cases (true_or_false (f b))) #fb 
-    [lapply (true_min …fb) //
+    [lapply (true_min …fb) #H >H >H //
     |>false_min // >false_min // @Hind /2/
     ]
   ]
@@ -298,7 +298,7 @@ min n b g ≤ min n b f.
 qed.
 
 theorem f_min_true : ∀ f.∀n,b.
-(∃i:nat. b ≤ i ∧ i < n ∧ f i = true) → f (min n b f) = true. 
+(∃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/
 qed.
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index bb77db7c6..7ca90dcb2 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -151,6 +151,9 @@ theorem associative_times: associative nat times.
 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
 // qed. 
 
+theorem times_n_1 : ∀n:nat. n = n * 1.
+#n // qed.
+
 (* ci servono questi risultati? 
 theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
 napply nat_elim2 /2/ 
@@ -452,58 +455,46 @@ cut (∀q:nat. q ≤ n → P q) /2/
 qed.
 
 (* some properties of functions *)
-(*
-definition increasing \def \lambda f:nat \to nat. 
-\forall n:nat. f n < f (S n).
-
-theorem increasing_to_monotonic: \forall f:nat \to nat.
-increasing f \to monotonic nat lt f.
-unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.
-apply (trans_le ? (f n1)).
-assumption.apply (trans_le ? (S (f n1))).
-apply le_n_Sn.
-apply H.
+
+definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
+
+theorem increasing_to_monotonic: ∀f:nat → nat.
+  increasing f → monotonic nat lt f.
+#f #incr #n #m #ltnm (elim ltnm) /2/
 qed.
 
-theorem le_n_fn: \forall f:nat \to nat. (increasing f) 
-\to \forall n:nat. n \le (f n).
-intros.elim n.
-apply le_O_n.
-apply (trans_le ? (S (f n1))).
-apply le_S_S.apply H1.
-simplify in H. unfold increasing in H.unfold lt in H.apply H.
+theorem le_n_fn: ∀f:nat → nat. 
+  increasing f → ∀n:nat. n ≤ f n.
+#f #incr #n (elim n) /2/
 qed.
 
-theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
-\to \forall m:nat. \exists i. m \le (f i).
-intros.elim m.
-apply (ex_intro ? ? O).apply le_O_n.
-elim H1.
-apply (ex_intro ? ? (S a)).
-apply (trans_le ? (S (f a))).
-apply le_S_S.assumption.
-simplify in H.unfold increasing in H.unfold lt in H.
-apply H.
+theorem increasing_to_le: ∀f:nat → nat. 
+  increasing f → ∀m:nat.∃i.m ≤ f i.
+#f #incr #m (elim m) /2/#n * #a #lenfa
+@(ex_intro ?? (S a)) /2/
 qed.
 
-theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) 
-\to \forall m:nat. (f O) \le m \to 
-\exists i. (f i) \le m \land m <(f (S i)).
-intros.elim H1.
-apply (ex_intro ? ? O).
-split.apply le_n.apply H.
-elim H3.elim H4.
-cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))).
-elim Hcut.
-apply (ex_intro ? ? a).
-split.apply le_S. assumption.assumption.
-apply (ex_intro ? ? (S a)).
-split.rewrite < H7.apply le_n.
-rewrite > H7.
-apply H.
-apply le_to_or_lt_eq.apply H6.
+theorem increasing_to_le2: ∀f:nat → nat. increasing f → 
+  ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
+#f #incr #m #lem (elim lem)
+  [@(ex_intro ? ? O) /2/
+  |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
+    [@(ex_intro ? ? a) % /2/ 
+    |@(ex_intro ? ? (S a)) % //
+    ]
+  ]
+qed.
+
+theorem increasing_to_injective: ∀f:nat → nat.
+  increasing f → injective nat nat f.
+#f #incr #n #m cases(decidable_le n m)
+  [#lenm cases(le_to_or_lt_eq … lenm) //
+   #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq 
+   @increasing_to_monotonic //
+  |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq 
+   @lt_to_not_eq @increasing_to_monotonic /2/
+  ]
 qed.
-*)
 
 (*********************** monotonicity ***************************)
 theorem monotonic_le_plus_r: 
@@ -692,8 +683,8 @@ simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
 apply lt_plus.assumption.assumption.
 qed. *)
 
-theorem monotonic_lt_times_l: 
-  ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+theorem monotonic_lt_times_r: 
+  ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
 #c #posc #n #m #ltnm
 (elim ltnm) normalize
   [/2/ 
@@ -701,9 +692,10 @@ theorem monotonic_lt_times_l:
   ]
 qed.
 
-theorem monotonic_lt_times_r: 
-  ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
-/2/ qed.
+theorem monotonic_lt_times_l: 
+  ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+/2/
+qed.
 
 theorem lt_to_le_to_lt_times: 
 ∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
diff --git a/matita/matita/lib/arithmetics/nth_prime.ma b/matita/matita/lib/arithmetics/nth_prime.ma
new file mode 100644
index 000000000..7b7c70bfe
--- /dev/null
+++ b/matita/matita/lib/arithmetics/nth_prime.ma
@@ -0,0 +1,201 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "nat/primes.ma".
+include "nat/lt_arith.ma".
+
+(* upper bound by Bertrand's conjecture. *)
+(* Too difficult to prove.        
+let rec nth_prime n \def
+match n with
+  [ O \Rightarrow (S(S O))
+  | (S p) \Rightarrow
+    let previous_prime \def S (nth_prime p) in
+    min_aux previous_prime ((S(S O))*previous_prime) primeb].
+
+theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
+normalize.reflexivity.
+qed.
+
+theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
+normalize.reflexivity.
+qed.
+
+theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
+qed. *)
+
+theorem smallest_factor_fact: \forall n:nat.
+n < smallest_factor (S n!).
+intros.
+apply not_le_to_lt.unfold Not.
+intro.
+apply (not_divides_S_fact n (smallest_factor(S n!))).
+apply lt_SO_smallest_factor.
+unfold lt.apply le_S_S.apply le_SO_fact.
+assumption.
+apply divides_smallest_factor_n.
+unfold lt.apply le_S_S.apply le_O_n.
+qed.
+
+theorem ex_prime: \forall n. (S O) \le n \to \exists m.
+n < m \land m \le S n! \land (prime m).
+intros.
+elim H.
+apply (ex_intro nat ? (S(S O))).
+split.split.apply (le_n (S(S O))).
+apply (le_n (S(S O))).apply (primeb_to_Prop (S(S O))).
+apply (ex_intro nat ? (smallest_factor (S (S n1)!))).
+split.split.
+apply smallest_factor_fact.
+apply le_smallest_factor_n.
+(* Andrea: ancora hint non lo trova *)
+apply prime_smallest_factor_n.unfold lt.
+apply le_S.apply le_SSO_fact.
+unfold lt.apply le_S_S.assumption.
+qed.
+
+let rec nth_prime n \def
+match n with
+  [ O \Rightarrow (S(S O))
+  | (S p) \Rightarrow
+    let previous_prime \def (nth_prime p) in
+    let upper_bound \def S previous_prime! in
+    min_aux upper_bound (S previous_prime) primeb].
+    
+(* it works
+theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
+normalize.reflexivity.
+qed.
+
+theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
+normalize.reflexivity.
+qed.
+
+theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
+qed.
+
+alias num (instance 0) = "natural number".
+theorem example14 : nth_prime 18 = 67.
+normalize.reflexivity.
+qed.
+*)
+
+theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
+intro.
+apply (nat_case n).simplify.
+apply (primeb_to_Prop (S(S O))).
+intro.
+change with
+(let previous_prime \def (nth_prime m) in
+let upper_bound \def S previous_prime! in
+prime (min_aux upper_bound (S previous_prime) primeb)).
+apply primeb_true_to_prime.
+apply f_min_aux_true.
+apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
+split.split.
+apply smallest_factor_fact.
+apply transitive_le;
+ [2: apply le_smallest_factor_n
+ | skip
+ | apply (le_plus_n_r (S (nth_prime m)) (S (fact (nth_prime m))))
+ ].
+apply prime_to_primeb_true.
+apply prime_smallest_factor_n.unfold lt.
+apply le_S_S.apply le_SO_fact.
+qed.
+
+(* properties of nth_prime *)
+theorem increasing_nth_prime: increasing nth_prime.
+unfold increasing.
+intros.
+change with
+(let previous_prime \def (nth_prime n) in
+let upper_bound \def S previous_prime! in
+(S previous_prime) \le min_aux upper_bound (S previous_prime) primeb).
+intros.
+apply le_min_aux.
+qed.
+
+variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat. 
+(nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
+
+theorem injective_nth_prime: injective nat nat nth_prime.
+apply increasing_to_injective.
+apply increasing_nth_prime.
+qed.
+
+theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
+intros. elim n.unfold lt.apply le_n.
+apply (trans_lt ? (nth_prime n1)).
+assumption.apply lt_nth_prime_n_nth_prime_Sn.
+qed.
+
+theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
+intros.apply (trans_lt O (S O)).
+unfold lt. apply le_n.apply lt_SO_nth_prime_n.
+qed.
+
+theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n.
+intro.
+elim n
+  [apply lt_O_nth_prime_n
+  |apply (lt_to_le_to_lt ? (S (nth_prime n1)))
+    [unfold.apply le_S_S.assumption
+    |apply lt_nth_prime_n_nth_prime_Sn
+    ]
+  ]
+qed.
+
+theorem ex_m_le_n_nth_prime_m: 
+\forall n: nat. nth_prime O \le n \to 
+\exists m. nth_prime m \le n \land n < nth_prime (S m).
+intros.
+apply increasing_to_le2.
+exact lt_nth_prime_n_nth_prime_Sn.assumption.
+qed.
+
+theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n) 
+\to \lnot (prime m).
+intros.
+apply primeb_false_to_not_prime.
+letin previous_prime \def (nth_prime n).
+letin upper_bound \def (S previous_prime!).
+apply (lt_min_aux_to_false primeb (S previous_prime) upper_bound m).
+assumption.
+unfold lt.
+apply (transitive_le (S m) (nth_prime (S n)) (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb) ? ?);
+  [apply (H1).
+  |apply (le_n (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb)).
+  ]
+qed.
+
+(* nth_prime enumerates all primes *)
+theorem prime_to_nth_prime : \forall p:nat. prime p \to
+\exists i. nth_prime i = p.
+intros.
+cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)).
+elim Hcut.elim H1.
+cut (nth_prime a < p \lor nth_prime a = p).
+elim Hcut1.
+absurd (prime p).
+assumption.
+apply (lt_nth_prime_to_not_prime a).assumption.assumption.
+apply (ex_intro nat ? a).assumption.
+apply le_to_or_lt_eq.assumption.
+apply ex_m_le_n_nth_prime_m.
+simplify.unfold prime in H.elim H.assumption.
+qed.
+
diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
new file mode 100644
index 000000000..2c4897d06
--- /dev/null
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -0,0 +1,530 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/factorial.ma".
+include "arithmetics/minimization.ma".
+
+inductive divides (n,m:nat) : Prop ≝
+quotient: ∀q:nat.m = times n q → divides n m.
+
+interpretation "divides" 'divides n m = (divides n m).
+interpretation "not divides" 'ndivides n m = (Not (divides n m)).
+
+theorem reflexive_divides : reflexive nat divides.
+/2/ qed.
+
+theorem divides_to_div_mod_spec :
+∀n,m. O < n → n ∣ m → div_mod_spec m n (m / n) O.
+#n #m #posn * #q #eqm % // >eqm 
+>commutative_times >div_times //
+qed.
+
+theorem div_mod_spec_to_divides :
+∀n,m,q. div_mod_spec m n q O → n ∣ m.
+#n #m #q * #posn #eqm /2/
+qed.
+
+theorem divides_to_mod_O:
+∀n,m. O < n → n ∣ m → (m \mod n) = O.
+#n #m #posn #divnm 
+@(div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O) /2/ 
+qed.
+
+theorem mod_O_to_divides:
+∀n,m. O < n → (m \mod n) = O →  n ∣ m. 
+/2/ qed.
+
+theorem divides_n_O: ∀n:nat. n ∣ O.
+/2/ qed.
+
+theorem divides_n_n: ∀n:nat. n ∣ n.
+/2/ qed.
+
+theorem divides_SO_n: ∀n:nat. 1 ∣ n.
+/2/ qed.
+
+theorem divides_plus: ∀n,p,q:nat. 
+n ∣ p → n ∣ q → n ∣ p+q.
+#n #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1+d2))
+>H >H1 //
+qed.
+
+theorem divides_minus: ∀n,p,q:nat. 
+n ∣ p → n ∣ q → n ∣ (p-q).
+#n #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1-d2))
+>H >H1 //
+qed.
+
+theorem divides_times: ∀n,m,p,q:nat. 
+n ∣ p → m ∣ q → n*m ∣ p*q.
+#n #m #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1*d2))
+>H >associative_times >associative_times @eq_f //
+qed.
+
+theorem transitive_divides: transitive ? divides.
+#a #b #c * #d1 #H * #d2 #H1 @(quotient ?? (d1*d2)) 
+>H1 >H //
+qed.
+
+theorem eq_mod_to_divides: ∀n,m,q. O < q →
+  mod n q = mod m q → q ∣ (n-m).
+#n #m #q #posq #eqmod @(leb_elim n m) #nm
+  [cut (n-m=O) /2/
+  |@(quotient ?? ((div n q)-(div m q)))
+   >distributive_times_minus >commutative_times
+   >(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H
+   >H >minus_minus >eqmod >commutative_plus 
+   <div_mod //
+  ]
+qed.
+
+theorem divides_to_le : ∀n,m. O < m → n ∣ m → n ≤ m.
+#n #m #posm * #d (cases d) 
+  [#eqm @False_ind /2/ |#p #eqm >eqm // ]
+qed.
+
+theorem antisymmetric_divides: ∀n,m. n ∣ m → m ∣ n → n = m.
+#n #m #divnm #divmn (cases (le_to_or_lt_eq … (le_O_n n))) #Hn
+  [(cases (le_to_or_lt_eq … (le_O_n m))) #Hm
+    [@le_to_le_to_eq @divides_to_le //
+    |<Hm (cases divmn) //
+    ]
+  |<Hn (cases divnm) //
+  ]
+qed.  
+
+theorem divides_to_lt_O : ∀n,m. O < m → n ∣ m → O < n.
+#n #m #posm (cases (le_to_or_lt_eq … (le_O_n n))) //
+#eqn0 * #d <eqn0 #eqm @False_ind @(absurd …posm) 
+@le_to_not_lt > eqm //
+qed.
+
+(*a variant of or_div_mod *)
+theorem or_div_mod1: ∀n,q. O < q →
+  q ∣ S n ∧ S n = S (n/q) * q ∨
+  q ∤ S n ∧ S n= (div n q) * q + S (n\mod q).
+#n #q #posq cases(or_div_mod n q posq) * #H1 #H2
+  [%1 % /2/
+  |%2 % // @(not_to_not ? ? (divides_to_mod_O … posq))
+   cut (S n \mod q = S(n \mod q)) 
+    [@(div_mod_spec_to_eq2 (S n) q (S n/q) (S n \mod q) (n/q) (S (n \mod q))) /2/]
+   #Hcut >Hcut % /2/
+  ]
+qed.
+
+theorem divides_to_div: ∀n,m.n ∣m → m/n*n = m.
+#n #m #divnm (cases (le_to_or_lt_eq O n (le_O_n n))) #H
+  [>(plus_n_O (m/n*n)) <(divides_to_mod_O ?? H divnm) //
+  |(cases divnm) #d <H //
+  ]
+qed.
+
+theorem divides_div: ∀d,n. d ∣ n → n/d ∣ n.
+#d #n #divdn @(quotient ?? d) @sym_eq /2/
+qed.
+
+theorem div_div: ∀n,d:nat. O < n → d ∣ n → n/(n/d) = d.
+#n #d #posn #divdn @(injective_times_l (n/d))
+  [@(lt_times_n_to_lt_l d) >divides_to_div //
+  |>divides_to_div 
+    [>commutative_times >divides_to_div //
+    |@(quotient ? ? d) @sym_eq /2/
+    ]
+  ]
+qed.
+
+theorem times_div: ∀a,b,c:nat.
+  O < b → c ∣ b → a * (b /c) = (a*b)/c.
+#a #b #c #posb #divcb 
+cut(O < c) [@(divides_to_lt_O … posb divcb)] #posc
+(cases divcb) #d #eqb >eqb
+>(commutative_times c d) >(div_times d c posc) <associative_times
+>(div_times (a * d) c posc) // 
+qed.
+
+theorem plus_div: ∀n,m,d. O < d →
+  d ∣ n → d ∣ m → (n + m) / d = n/d + m/d.
+#n #m #d #posd #divdn #divdm
+(cases divdn) #a #eqn (cases divdm) #b #eqm
+>eqn >eqm <distributive_times_plus >commutative_times
+>div_times // >commutative_times >div_times //
+>commutative_times >div_times //
+qed.
+
+(* boolean divides *)
+definition dividesb : nat → nat → bool ≝
+λn,m :nat. (eqb (m \mod n) O).
+
+theorem dividesb_true_to_divides:
+∀n,m:nat. dividesb n m = true → n ∣ m.
+#n #m (cases (le_to_or_lt_eq … (le_O_n n)))
+  [#posn #divbnm @mod_O_to_divides // @eqb_true_to_eq @divbnm 
+  |#eqnO <eqnO normalize #eqbmO >(eqb_true_to_eq … eqbmO) //
+  ]
+qed.
+
+theorem dividesb_false_to_not_divides:
+∀n,m:nat. dividesb n m = false → n ∤ m.
+#n #m (cases (le_to_or_lt_eq … (le_O_n n)))
+  [#posn #ndivbnm @(not_to_not ?? (divides_to_mod_O … posn))
+   @eqb_false_to_not_eq @ndivbnm
+  |#eqnO <eqnO normalize 
+   @(nat_case m) [normalize /2/ |#a #_ #_ % * /2/]
+  ]
+qed.
+
+theorem decidable_divides: ∀n,m:nat. decidable (n ∣ m).
+#n #m cases(true_or_false (dividesb n m)) /3/
+qed.
+
+theorem divides_to_dividesb_true : ∀n,m:nat. O < n →
+  n ∣m → dividesb n m = true.
+#n #m #posn #divnm cases(true_or_false (dividesb n m)) //
+#ndivbnm @False_ind @(absurd … divnm) /2/
+qed.
+
+theorem divides_to_dividesb_true1 : ∀n,m:nat.O < m → 
+  n ∣m → dividesb n m = true.
+#n #m #posn cases (le_to_or_lt_eq O n (le_O_n n)) /2/
+#eqn0 <eqn0 * #q #eqm @False_ind /2/
+qed.
+
+theorem not_divides_to_dividesb_false: ∀n,m:nat. O < n →
+  n ∤ m → dividesb n m = false.
+#n #m #posn cases(true_or_false (dividesb n m)) /2/
+#divbnm #ndivnm @False_ind @(absurd ?? ndivnm) /2/
+qed.
+
+theorem dividesb_div_true: 
+∀d,n. O < n → 
+  dividesb d n = true → dividesb (n/d) n = true.
+#d #n #posn #divbdn @divides_to_dividesb_true1 //
+@divides_div /2/
+qed.
+
+theorem dividesb_true_to_lt_O: ∀n,m. 
+  O < n → m ∣ n → O < m.
+#n #m #posn * #d cases (le_to_or_lt_eq ? ? (le_O_n m)) // 
+qed.
+
+(* divides and pi move away ??
+theorem divides_f_pi_f : ∀f:nat → nat.∀n,i:nat. 
+  i < n → f i ∣ \big[times,0]_{x < n | true}(f x).
+#f #n #i (elim n) 
+  [#ltiO @False_ind /2/
+  |#n #Hind #lti >bigop_Strue // 
+   cases(le_to_or_lt_eq …(le_S_S_to_le … lti)) /3/
+  ]
+*)
+
+(* prime *)
+definition prime : nat → Prop ≝
+λn:nat. 1 < n ∧ (∀m:nat. m ∣ n → 1 < m → m = n).
+
+theorem not_prime_O: ¬ (prime O).
+% * #lt10 /2/
+qed.
+
+theorem not_prime_SO: ¬ (prime 1).
+% * #lt11 /2/
+qed.
+
+theorem prime_to_lt_O: ∀p. prime p → O < p.
+#p * #lt1p /2/ 
+qed.
+
+theorem prime_to_lt_SO: ∀p. prime p → 1 < p.
+#p * #lt1p /2/ 
+qed.
+
+(* smallest factor *)
+definition smallest_factor : nat → nat ≝
+λn:nat. if_then_else ? (leb n 1) n
+  (min n 2 (λm.(eqb (n \mod m) O))).
+
+theorem smallest_factor_to_min : ∀n. 1 < n → 
+smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))).
+#n #lt1n normalize >lt_to_leb_false //
+qed.
+
+(* it works ! 
+theorem example1 : smallest_factor 3 = 3.
+normalize //
+qed.
+
+theorem example2: smallest_factor 4 = 2.
+normalize //
+qed.
+
+theorem example3 : smallest_factor 7 = 7.
+normalize //
+qed. *)
+
+theorem le_SO_smallest_factor: ∀n:nat. 
+  n ≤ 1 → smallest_factor n = n.
+#n #le1n normalize >le_to_leb_true //
+qed.
+
+theorem lt_SO_smallest_factor: ∀n:nat. 
+  1 < n → 1 < smallest_factor n.
+#n #lt1n >smallest_factor_to_min //
+qed.
+
+theorem lt_O_smallest_factor: ∀n:nat. 
+  O < n → O < (smallest_factor n).
+#n #posn (cases posn) 
+  [>le_SO_smallest_factor //
+  |#m #posm @le_S_S_to_le @le_S @lt_SO_smallest_factor @le_S_S //
+  ]
+qed.
+
+theorem divides_smallest_factor_n : ∀n:nat. 0 < n → 
+  smallest_factor n ∣ n.
+#n #posn (cases (le_to_or_lt_eq … posn)) 
+  [#lt1n @mod_O_to_divides [@lt_O_smallest_factor //] 
+   >smallest_factor_to_min // @eqb_true_to_eq @f_min_true
+   @(ex_intro … n) % /2/ @eq_to_eqb_true /2/
+  |#H <H //
+  ]
+qed.
+  
+theorem le_smallest_factor_n : ∀n.
+  smallest_factor n ≤ n.
+#n (cases n) // #m @divides_to_le /2/
+qed.
+
+theorem lt_smallest_factor_to_not_divides: ∀n,i:nat. 
+1 < n → 1 < i → i < smallest_factor n → i ∤ n.
+#n #i #ltn #lti >smallest_factor_to_min // #ltmin 
+@(not_to_not ? (n \mod i = 0))
+  [#divin @divides_to_mod_O /2/
+  |@eqb_false_to_not_eq @(lt_min_to_false … lti ltmin)
+  ]
+qed.
+
+theorem prime_smallest_factor_n : ∀n. 1 < n → 
+  prime (smallest_factor n).
+#n #lt1n (cut (0<n)) [/2/] #posn % /2/ #m #divmmin #lt1m
+@le_to_le_to_eq
+  [@divides_to_le // @lt_O_smallest_factor //
+  |>smallest_factor_to_min // @true_to_le_min //
+   @eq_to_eqb_true @divides_to_mod_O /2/ 
+   @(transitive_divides … divmmin) @divides_smallest_factor_n //
+  ]
+qed.
+
+theorem prime_to_smallest_factor: ∀n. prime n →
+  smallest_factor n = n.
+#n * #lt1n #primen @primen 
+  [@divides_smallest_factor_n /2/
+  |@lt_SO_smallest_factor //
+  ]
+qed.
+
+theorem smallest_factor_to_prime: ∀n. 1 < n →
+  smallest_factor n = n → prime n.
+#n #lt1n #H <H /2/ 
+qed.
+
+(* a number n > O is prime iff its smallest factor is n *)
+definition primeb ≝ λn:nat.
+  (leb 2 n) ∧ (eqb (smallest_factor n) n).
+
+(* it works! *)
+theorem example4 : primeb 3 = true.
+normalize // qed.
+
+theorem example5 : primeb 6 = false.
+normalize // qed.
+
+theorem example6 : primeb 11 = true.
+normalize // qed.
+
+theorem example7 : primeb 17 = true.
+normalize // qed.
+
+theorem primeb_true_to_prime : ∀n:nat.
+  primeb n = true → prime n.
+#n #primebn @smallest_factor_to_prime
+  [@leb_true_to_le @(andb_true_l … primebn)
+  |@eqb_true_to_eq @( andb_true_r … primebn)
+  ]
+qed.
+
+theorem primeb_false_to_not_prime : ∀n:nat.
+  primeb n = false → ¬ (prime n).
+#n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [>H //] 
+@leb_elim 
+  [#_ #H1 @(not_to_not … (prime_to_smallest_factor … ))
+   @eqb_false_to_not_eq @H1
+  |#len1 #_ @(not_to_not … len1) * //
+  ]
+qed.
+
+theorem decidable_prime : ∀n:nat.decidable (prime n).
+#n cases(true_or_false (primeb n)) #H 
+  [%1 /2/ |%2 /2/]
+qed.
+
+theorem prime_to_primeb_true: ∀n:nat. 
+  prime n → primeb n = true.
+#n #primen (cases (true_or_false (primeb n))) //
+#H @False_ind @(absurd … primen) /2/
+qed.
+
+theorem not_prime_to_primeb_false: ∀n:nat. 
+ ¬(prime n) → primeb n = false.
+#n #np (cases (true_or_false (primeb n))) //
+#p @False_ind @(absurd (prime n) (primeb_true_to_prime …) np) //
+qed.
+
+(* enumeration of all primes *)
+
+theorem divides_fact : ∀n,i:nat. O < i → 
+  i ≤ n → i ∣ n!.
+#n #i #ltOi (elim n) 
+  [#leiO @False_ind @(absurd … ltOi) /2/
+  |#n #Hind #lei normalize cases(le_to_or_lt_eq … lei)
+    [#ltiS @(transitive_divides ? n!) [@Hind /2/ | /2/]
+    |#eqi >eqi /2/
+    ]
+  ]
+qed.
+
+theorem mod_S_fact: ∀n,i:nat. 
+  1 < i → i ≤ n → (S n!) \mod i = 1.
+#n #i #lt1i #lein
+cut(O<i) [/2/] #posi
+cut (n! \mod i = O) [@divides_to_mod_O // @divides_fact //] #Hcut
+<Hcut @mod_S //
+qed.
+
+theorem not_divides_S_fact: ∀n,i:nat. 
+  1 < i → i ≤ n → i ∤  S n!.
+#n #i #lt1i #lein @(not_to_not … (divides_to_mod_O i (S n!) ?)) /2/
+>mod_S_fact // @eqb_false_to_not_eq //
+qed.
+
+theorem smallest_factor_fact: ∀n:nat.
+  n < smallest_factor (S n!).
+#n @not_le_to_lt @(not_to_not ? ((smallest_factor (S n!)) ∤ (S n!)))
+  [@not_divides_S_fact @lt_SO_smallest_factor @le_S_S //
+  |% * #H @H @divides_smallest_factor_n @le_S_S //
+  ]
+qed.
+
+theorem ex_prime: ∀n. 1 ≤ n →∃m.
+  n < m ∧ m ≤ S n! ∧ (prime m).
+#n #lein (cases lein)
+  [@(ex_intro nat ? 2) % [/2/|@primeb_true_to_prime //]
+  |#m #leim @(ex_intro nat ? (smallest_factor (S (S m)!)))
+   % [% [@smallest_factor_fact |@le_smallest_factor_n ]
+     |@prime_smallest_factor_n @le_S_S //
+     ]
+  ] 
+qed. 
+
+let rec nth_prime n ≝ match n with
+  [ O ⇒ 2
+  | S p ⇒
+    let previous_prime ≝ nth_prime p in
+    let upper_bound ≝ S previous_prime! in
+    min upper_bound (S previous_prime) primeb].
+
+lemma nth_primeS: ∀n.nth_prime (S n) = 
+  let previous_prime ≝ nth_prime n in
+    let upper_bound ≝ S previous_prime! in
+    min upper_bound (S previous_prime) primeb.
+// qed.
+    
+(* it works *)
+theorem example11 : nth_prime 2 = 5.
+normalize // qed.
+
+theorem example12: nth_prime 3 = 7.
+normalize //
+qed.
+
+theorem example13 : nth_prime 4 = 11.
+normalize // qed.
+
+(* done in 13.1369330883s -- qualcosa non va: // lentissimo 
+theorem example14 : nth_prime 18 = 67.
+normalize // (* @refl *)
+qed.
+*)
+
+theorem prime_nth_prime : ∀n:nat.prime (nth_prime n).
+#n (cases n) 
+  [@primeb_true_to_prime //
+  |#m >nth_primeS @primeb_true_to_prime @f_min_true
+   @(ex_intro nat ? (smallest_factor (S (nth_prime m)!)))
+   % [% // @le_S_S @(transitive_le … (le_smallest_factor_n …))
+      <plus_n_Sm @le_plus_n_r
+     ]
+   @prime_to_primeb_true @prime_smallest_factor_n @le_S_S //
+  ]
+qed.
+
+(* properties of nth_prime *)
+theorem increasing_nth_prime: ∀n. nth_prime n < nth_prime (S n).
+#n 
+change with
+(let previous_prime ≝ (nth_prime n) in
+ let upper_bound ≝ S previous_prime! in
+ S previous_prime ≤ min upper_bound (S previous_prime) primeb)
+apply le_min_l
+qed.
+
+theorem lt_SO_nth_prime_n : ∀n:nat. 1 < nth_prime n.
+#n @prime_to_lt_SO //
+qed.
+
+theorem lt_O_nth_prime_n : ∀n:nat. O < nth_prime n.
+#n @prime_to_lt_O //
+qed.
+
+theorem lt_n_nth_prime_n : ∀n:nat. n < nth_prime n.
+#n (elim n)
+  [@lt_O_nth_prime_n
+  |#m #ltm @(le_to_lt_to_lt … ltm) //
+  ]
+qed.
+
+(*
+theorem ex_m_le_n_nth_prime_m: 
+∀n.nth_prime O ≤ n → 
+∃m. nth_prime m ≤ n ∧ n < nth_prime (S m).
+intros.
+apply increasing_to_le2.
+exact lt_nth_prime_n_nth_prime_Sn.assumption.
+qed. *)
+
+theorem lt_nth_prime_to_not_prime: ∀n,m. 
+  nth_prime n < m → m < nth_prime (S n) → ¬ (prime m).
+#n #m #ltml >nth_primeS #ltmr @primeb_false_to_not_prime
+@(lt_min_to_false ? (S (nth_prime n)!) m (S (nth_prime n))) //
+qed.
+
+(* nth_prime enumerates all primes *)
+theorem prime_to_nth_prime : ∀p:nat. 
+  prime p → ∃i.nth_prime i = p.
+#p #primep
+cut (∃m. nth_prime m ≤ p ∧ p < nth_prime (S m))
+ [@(increasing_to_le2 nth_prime ?) // @prime_to_lt_SO //
+ |* #n * #lepl #ltpr cases(le_to_or_lt_eq … lepl)
+   [#ltpl @False_ind @(absurd … primep)
+    @(lt_nth_prime_to_not_prime n p ltpl ltpr)
+   |#eqp @(ex_intro … n) //
+   ]
+ ]
+qed.
+ 
diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma
new file mode 100644
index 000000000..adbfd9cab
--- /dev/null
+++ b/matita/matita/lib/basics/bool.ma
@@ -0,0 +1,76 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_______________________________________________________________ *)
+
+include "basics/relations.ma".
+
+(********** bool **********)
+inductive bool: Type[0] ≝ 
+  | true : bool
+  | false : bool.
+
+(* destruct does not work *)
+theorem not_eq_true_false : true ≠ false.
+@nmk #Heq change with match true with [true ⇒ False|false ⇒ True]
+>Heq // qed.
+
+definition notb : bool → bool ≝
+λ b:bool. match b with [true ⇒ false|false ⇒ true ].
+
+interpretation "boolean not" 'not x = (notb x).
+
+theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
+match b with
+[ true ⇒ P false
+| false ⇒ P true] → P (notb b).
+#b #P elim b normalize // qed.
+
+theorem notb_notb: ∀b:bool. notb (notb b) = b.
+#b elim b // qed.
+
+theorem injective_notb: injective bool bool notb.
+#b1 #b2 #H // qed.
+
+definition andb : bool → bool → bool ≝
+λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
+
+interpretation "boolean and" 'and x y = (andb x y).
+
+theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
+match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
+#b1 #b2 #P (elim b1) normalize // qed.
+
+theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
+#b1 (cases b1) normalize // qed.
+
+theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
+#b1 #b2 (cases b1) normalize // (cases b2) // qed.
+
+definition orb : bool → bool → bool ≝
+λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
+ 
+interpretation "boolean or" 'or x y = (orb x y).
+
+theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
+match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
+#b1 #b2 #P (elim b1) normalize // qed.
+
+definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝ 
+λA.λb.λ P,Q:A. match b with [ true ⇒ P | false  ⇒ Q].
+
+theorem bool_to_decidable_eq: 
+  ∀b1,b2:bool. decidable (b1=b2).
+#b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
+
+theorem true_or_false:
+∀b:bool. b = true ∨ b = false.
+#b (cases b) /2/ qed.
+
+
diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma
new file mode 100644
index 000000000..cdb497371
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation.ma
@@ -0,0 +1,287 @@
+(* exists *******************************************************************)
+
+notation "hvbox(∃ _ break . p)"
+ with precedence 20
+for @{'exists $p }.
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20
+for @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\exists ident i break . p)"
+  with precedence 20
+for @{'exists (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\exists ident i opt (: ty) break . p)"
+  right associative with precedence 20
+for @{ 'exists ${default
+  @{\lambda ${ident i} : $ty. $p}
+  @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
+  with precedence 20
+  for ${ default
+          @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
+          @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
+       }.
+
+(* sigma ********************************************************************)
+
+notation < "hvbox(\Sigma ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\Sigma ident i break . p)"
+ with precedence 20
+for @{'sigma (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
+  right associative with precedence 20
+for @{ 'sigma ${default
+  @{\lambda ${ident i} : $ty. $p}
+  @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
+  with precedence 20
+  for ${ default
+          @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
+          @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
+       }.
+
+(* equality, conguence ******************************************************)
+
+notation > "hvbox(a break = b)" 
+  non associative with precedence 45
+for @{ 'eq ? $a $b }.
+
+notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)" 
+  non associative with precedence 45
+for @{ 'eq $t $a $b }.
+
+notation > "hvbox(n break (≅ \sub term 90 p) m)"
+  non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
+  non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+(* other notations **********************************************************)
+
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
+with precedence 90 for @{ 'pair $a $b}.
+
+notation "hvbox(x break \times y)" with precedence 70
+for @{ 'product $x $y}.
+
+notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
+
+notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
+
+notation > "\fst" with precedence 90 for @{'pi1}.
+notation > "\snd" with precedence 90 for @{'pi2}.
+
+notation "hvbox(a break \to b)" 
+  right associative with precedence 20
+for @{ \forall $_:$a.$b }.
+
+notation < "hvbox(a break \to b)" 
+  right associative with precedence 20
+for @{ \Pi $_:$a.$b }.
+
+notation "hvbox(a break \leq b)" 
+  non associative with precedence 45
+for @{ 'leq $a $b }.
+
+notation "hvbox(a break \geq b)" 
+  non associative with precedence 45
+for @{ 'geq $a $b }.
+
+notation "hvbox(a break \lt b)" 
+  non associative with precedence 45
+for @{ 'lt $a $b }.
+
+notation "hvbox(a break \gt b)" 
+  non associative with precedence 45
+for @{ 'gt $a $b }.
+
+notation > "hvbox(a break \neq b)" 
+  non associative with precedence 45
+for @{ 'neq ? $a $b }.
+
+notation < "hvbox(a break maction (\neq) (\neq\sub t) b)" 
+  non associative with precedence 45
+for @{ 'neq $t $a $b }.
+
+notation "hvbox(a break \nleq b)" 
+  non associative with precedence 45
+for @{ 'nleq $a $b }.
+
+notation "hvbox(a break \ngeq b)" 
+  non associative with precedence 45
+for @{ 'ngeq $a $b }.
+
+notation "hvbox(a break \nless b)" 
+  non associative with precedence 45
+for @{ 'nless $a $b }.
+
+notation "hvbox(a break \ngtr b)" 
+  non associative with precedence 45
+for @{ 'ngtr $a $b }.
+
+notation "hvbox(a break \divides b)"
+  non associative with precedence 45
+for @{ 'divides $a $b }.
+
+notation "hvbox(a break \ndivides b)"
+  non associative with precedence 45
+for @{ 'ndivides $a $b }.
+
+notation "hvbox(a break + b)" 
+  left associative with precedence 50
+for @{ 'plus $a $b }.
+
+notation "hvbox(a break - b)" 
+  left associative with precedence 50
+for @{ 'minus $a $b }.
+
+notation "hvbox(a break * b)" 
+  left associative with precedence 55
+for @{ 'times $a $b }.
+
+notation "hvbox(a break \middot b)" 
+  left associative with precedence 55
+  for @{ 'middot $a $b }.
+
+notation "hvbox(a break \mod b)" 
+  left associative with precedence 55
+for @{ 'module $a $b }.
+
+notation < "a \frac b" 
+  non associative with precedence 90
+for @{ 'divide $a $b }.
+
+notation "a \over b" 
+  left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "hvbox(a break / b)" 
+  left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "- term 60 a" with precedence 60 
+for @{ 'uminus $a }.
+
+notation "a !"
+  non associative with precedence 80
+for @{ 'fact $a }.
+
+notation "\sqrt a" 
+  non associative with precedence 60
+for @{ 'sqrt $a }.
+
+notation "hvbox(a break \lor b)" 
+  left associative with precedence 30
+for @{ 'or $a $b }.
+
+notation "hvbox(a break \land b)" 
+  left associative with precedence 35
+for @{ 'and $a $b }.
+
+notation "hvbox(\lnot a)" 
+  non associative with precedence 40
+for @{ 'not $a }.
+
+notation > "hvbox(a break \liff b)" 
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)" 
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" left associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" left associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45 
+  for @{ 'napart $a $b}.
+        
+notation "hvbox(a break # b)" non associative with precedence 45 
+  for @{ 'apart $a $b}.
+    
+notation "hvbox(a break \circ b)" 
+  left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
+notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
+
+notation "↑a" with precedence 55 for @{ 'uparrow $a }.
+
+notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
+
+notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a ^ term 90 b"  non associative with precedence 75 for @{ 'exp $a $b}.
+notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}. 
+
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
+
+notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
+notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation > "⊩ " with precedence 60 for @{'Vdash ?}.
+notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+
+notation < "maction (mstyle color #ff0000 (­…­)) (t)" 
+non associative with precedence 90 for @{'hide $t}.
\ No newline at end of file
diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
new file mode 100644
index 000000000..ad3aa9371
--- /dev/null
+++ b/matita/matita/lib/basics/jmeq.ma
@@ -0,0 +1,92 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "basics/logic.ma".
+
+inductive Sigma: Type[1] ≝
+ mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
+
+definition p1: Sigma → Type[0].
+ #S cases S #Y #_ @Y
+qed.
+
+definition p2: ∀S:Sigma. p1 S.
+ #S cases S #Y #x @x
+qed.
+
+inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
+jmrefl : jmeq A x A x.
+
+definition eqProp ≝ λA:Prop.eq A.
+
+lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
+#A #x #h @(refl ? h: eqProp ? ? ?).
+qed.
+
+definition cast:
+ ∀A,B:Type[0].∀E:A=B. A → B.
+ #A #B #E cases E #X @X
+qed.
+
+lemma tech1:
+ ∀Aa,Bb:Sigma.∀E:Aa=Bb.
+  cast (p1 Aa) (p1 Bb) ? (p2 Aa) = p2 Bb.
+ [2: >E %
+ | #Aa #Bb #E >E cases Bb #B #b normalize % ]
+qed.
+ 
+lemma gral: ∀A.∀x,y:A.
+ mk_Sigma A x = mk_Sigma A y → x=y.
+ #A #x #y #E lapply (tech1 ?? E)
+ generalize in ⊢ (??(???%?)? → ?) #E1
+ normalize in E1; >(K ?? E1) normalize
+ #H @H
+qed.
+
+axiom daemon: False.
+
+lemma jm_to_eq_sigma:
+ ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
+ #A #x #y #E cases E in ⊢ (???%); %
+qed.
+
+definition curry:
+ ∀A,x.
+  (∀y. jmeq A x A y → Type[0]) →
+   (∀y. mk_Sigma A x = mk_Sigma A y → Type[0]).
+ #A #x #f #y #E @(f y) >(gral ??? E) %
+qed.
+
+lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
+ P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
+  P y h.
+ #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
+ @(match G
+    return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
+   with
+    [refl ⇒ ?])
+ #E <(sym_eq ??? (K ?? E)) @H
+qed.
+
+definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
+ #A #P #a @(P a)
+qed.
+
+lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
+ PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
+ #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
+ lapply (G ?? (curry ?? P) ?? F)
+  [ normalize //
+  | #H whd in H; @(H : PP ? (P b) ?) ]
+qed.
+
+lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
+ P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.
diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
new file mode 100644
index 000000000..4d99c59c8
--- /dev/null
+++ b/matita/matita/lib/basics/list.ma
@@ -0,0 +1,170 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_______________________________________________________________ *)
+
+include "basics/types.ma".
+include "basics/bool.ma".
+
+inductive list (A:Type[0]) : Type[0] :=
+  | nil: list A
+  | cons: A -> list A -> list A.
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+definition not_nil: ∀A:Type[0].list A → Prop ≝
+ λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
+
+theorem nil_cons:
+  ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
+  #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+qed.
+
+(*
+let rec id_list A (l: list A) on l :=
+  match l with
+  [ nil => []
+  | (cons hd tl) => hd :: id_list A tl ]. *)
+
+let rec append A (l1: list A) l2 on l1 ≝ 
+  match l1 with
+  [ nil ⇒  l2
+  | cons hd tl ⇒  hd :: append A tl l2 ].
+
+definition hd ≝ λA.λl: list A.λd:A.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+definition tail ≝  λA.λl: list A.
+  match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+theorem append_nil: ∀A.∀l:list A.l @ [] = l.
+#A #l (elim l) normalize // qed.
+
+theorem associative_append: 
+ ∀A.associative (list A) (append A).
+#A #l1 #l2 #l3 (elim l1) normalize // qed.
+
+(* deleterio per auto 
+ntheorem cons_append_commute:
+  ∀A:Type.∀l1,l2:list A.∀a:A.
+    a :: (l1 @ l2) = (a :: l1) @ l2.
+//; nqed. *)
+
+theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
+/2/ qed.
+
+theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
+  l1@l2=[] → P (nil A) (nil A) → P l1 l2.
+#A #l1 #l2 #P (cases l1) normalize //
+#a #l3 #heq destruct
+qed.
+
+theorem nil_to_nil:  ∀A.∀l1,l2:list A.
+  l1@l2 = [] → l1 = [] ∧ l2 = [].
+#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
+qed.
+
+(* iterators *)
+
+let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
+ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+  
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+ 
+definition filter ≝ 
+  λT.λp:T → bool.
+  foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
+
+lemma filter_true : ∀A,l,a,p. p a = true → 
+  filter A p (a::l) = a :: filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+lemma filter_false : ∀A,l,a,p. p a = false → 
+  filter A p (a::l) = filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+#A #B #f #g #l #eqfg (elim l) normalize // qed.
+
+let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
+match l1 with
+  [ nil ⇒ nil ?
+  | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
+  ].
+
+(**************************** fold *******************************)
+
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
+ match l with 
+  [ nil ⇒ b 
+  | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
+      (fold A B op b p f l)].
+      
+notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
+  with precedence 80
+for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
+
+notation "\fold [ op , nil ]_{ident i ∈ l } f"
+  with precedence 80
+for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
+
+interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
+
+theorem fold_true: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
+  \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
+    op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_false: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
+p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
+  \fold[op,nil]_{i ∈ l| p i} (f i).
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_filter: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
+  \fold[op,nil]_{i ∈ l| p i} (f i) = 
+    \fold[op,nil]_{i ∈ (filter A p l)} (f i).
+#A #B #a #l #p #op #nil #f elim l //  
+#a #tl #Hind cases(true_or_false (p a)) #pa 
+  [ >filter_true // > fold_true // >fold_true //
+  | >filter_false // >fold_false // ]
+qed.
+
+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
+  }.
+
+theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
+  op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
+    \fold[op,nil]_{i∈(I@J)} (f i).
+#A #B #I #J #nil #op #f (elim I) normalize 
+  [>nill //|#a #tl #Hind <assoc //]
+qed.
+
diff --git a/matita/matita/lib/basics/list2.ma b/matita/matita/lib/basics/list2.ma
new file mode 100644
index 000000000..1dd62c114
--- /dev/null
+++ b/matita/matita/lib/basics/list2.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basics/list.ma".
+include "arithmetics/nat.ma".
+
+nlet rec length (A:Type) (l:list A) on l ≝ 
+  match l with 
+    [ nil ⇒ 0
+    | cons a tl ⇒ S (length A tl)].
+
+notation "|M|" non associative with precedence 60 for @{'norm $M}.
+interpretation "norm" 'norm l = (length ? l).
+
+nlet rec nth n (A:Type) (l:list A) (d:A)  ≝  
+  match n with
+    [O ⇒ hd A l d
+    |S m ⇒ nth m A (tail A l) d].
+
diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
new file mode 100644
index 000000000..43bbcbc4b
--- /dev/null
+++ b/matita/matita/lib/basics/logic.ma
@@ -0,0 +1,221 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_______________________________________________________________ *)
+
+include "basics/pts.ma".
+include "hints_declaration.ma".
+
+(* propositional equality *)
+
+inductive eq (A:Type[1]) (x:A) : A → Prop ≝
+    refl: eq A x x. 
+    
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+
+lemma eq_rect_r:
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
+ #A #a #x #p (cases p) // qed.
+
+lemma eq_ind_r :
+ ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
+
+lemma eq_rect_Type2_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+  cases p; //; qed.
+
+theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x = y → P y.
+#A #x #P #Hx #y #Heq (cases Heq); //; qed.
+
+theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
+#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
+
+theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y = x → P y.
+#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
+
+theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
+#A #B #Ha #Heq (elim Heq); //; qed.
+
+theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
+#A #x #y #z #H1 #H2 >H1; //; qed.
+
+theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
+#A #B #f #x #y #H >H; //; qed.
+
+(* deleterio per auto? *)
+theorem eq_f2: ∀A,B,C.∀f:A→B→C.
+∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
+#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. 
+
+(* hint to genereric equality 
+definition eq_equality: equality ≝
+ mk_equality eq refl rewrite_l rewrite_r.
+
+
+unification hint 0 ≔ T,a,b;
+ X ≟ eq_equality
+(*------------------------------------*) ⊢
+    equal X T a b ≡ eq T a b.
+*)
+  
+(********** connectives ********)
+
+inductive True: Prop ≝  
+I : True.
+
+inductive False: Prop ≝ .
+
+(* ndefinition Not: Prop → Prop ≝
+λA. A → False. *)
+
+inductive Not (A:Prop): Prop ≝
+nmk: (A → False) → Not A.
+
+interpretation "logical not" 'not x = (Not x).
+
+theorem absurd : ∀A:Prop. A → ¬A → False.
+#A #H #Hn (elim Hn); /2/; qed.
+
+(*
+ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
+#A; #C; #H; #Hn; nelim (Hn H).
+nqed. *)
+
+theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+/4/; qed.
+
+(* inequality *)
+interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
+
+theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
+/3/; qed.
+
+(* and *)
+inductive And (A,B:Prop) : Prop ≝
+    conj : A → B → And A B.
+
+interpretation "logical and" 'and x y = (And x y).
+
+theorem proj1: ∀A,B:Prop. A ∧ B → A.
+#A #B #AB (elim AB) //; qed.
+
+theorem proj2: ∀ A,B:Prop. A ∧ B → B.
+#A #B #AB (elim AB) //; qed.
+
+(* or *)
+inductive Or (A,B:Prop) : Prop ≝
+     or_introl : A → (Or A B)
+   | or_intror : B → (Or A B).
+
+interpretation "logical or" 'or x y = (Or x y).
+
+definition decidable : Prop → Prop ≝ 
+λ A:Prop. A ∨ ¬ A.
+
+(* exists *)
+inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
+    ex_intro: ∀ x:A. P x →  ex A P.
+    
+interpretation "exists" 'exists x = (ex ? x).
+
+inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
+    ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
+
+(* iff *)
+definition iff :=
+ λ A,B. (A → B) ∧ (B → A).
+
+interpretation "iff" 'iff a b = (iff a b).  
+
+(* cose per destruct: da rivedere *) 
+
+definition R0 ≝ λT:Type[0].λt:T.t.
+  
+definition R1 ≝ eq_rect_Type0.
+
+(* 
+definition R2 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  T2 b0 e0 b1 e1.
+#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
+napply (eq_rect_Type0 ????? e1);
+napply (R1 ?? ? ?? e0);
+napply a2;
+nqed.
+
+ndefinition R3 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+  ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+  T3 b0 e0 b1 e1 b2 e2.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
+napply (eq_rect_Type0 ????? e2);
+napply (R2 ?? ? ???? e0 ? e1);
+napply a3;
+nqed.
+
+ndefinition R4 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+  ∀a1:T1 a0 (refl T0 a0).
+  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+  ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
+  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+  ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2). 
+  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+      ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. 
+      Type[0].
+  ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2) 
+      a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+                   a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
+                   a3).
+  ∀b0:T0.
+  ∀e0:eq (T0 …) a0 b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+  ∀b3: T3 b0 e0 b1 e1 b2 e2.
+  ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+  T4 b0 e0 b1 e1 b2 e2 b3 e3.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
+napply (eq_rect_Type0 ????? e3);
+napply (R3 ????????? e0 ? e1 ? e2);
+napply a4;
+nqed.
+
+naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. *)
diff --git a/matita/matita/lib/basics/pts.ma b/matita/matita/lib/basics/pts.ma
new file mode 100644
index 000000000..94f49fc5c
--- /dev/null
+++ b/matita/matita/lib/basics/pts.ma
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basics/core_notation.ma".
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+universe constraint Type[2] < Type[3].
+universe constraint Type[3] < Type[4].
diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
new file mode 100644
index 000000000..b31db23d7
--- /dev/null
+++ b/matita/matita/lib/basics/relations.ma
@@ -0,0 +1,106 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "basics/logic.ma".
+
+(********** relations **********)
+definition relation : Type[0] → Type[0]
+≝ λA.A→A→Prop. 
+
+definition reflexive: ∀A.∀R :relation A.Prop
+≝ λA.λR.∀x:A.R x x.
+
+definition symmetric: ∀A.∀R: relation A.Prop
+≝ λA.λR.∀x,y:A.R x y → R y x.
+
+definition transitive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
+
+definition irreflexive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x:A.¬(R x x).
+
+definition cotransitive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
+
+definition tight_apart: ∀A.∀eq,ap:relation A.Prop
+≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
+(eq x y → ¬(ap x y)).
+
+definition antisymmetric: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
+
+(********** functions **********)
+
+definition compose ≝
+  λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
+
+interpretation "function composition" 'compose f g = (compose ? ? ? f g).
+
+definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
+≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
+
+definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
+≝λA,B.λf.∀z:B.∃x:A.z = f x.
+
+definition commutative: ∀A:Type[0].∀f:A→A→A.Prop 
+≝ λA.λf.∀x,y.f x y = f y x.
+
+definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
+≝ λA,B.λf.∀x,y.f x y = f y x.
+
+definition associative: ∀A:Type[0].∀f:A→A→A.Prop
+≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
+
+(* functions and relations *)
+definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
+∀f:A→A.Prop ≝
+λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
+
+(* functions and functions *)
+definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
+≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
+
+definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
+≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
+
+lemma injective_compose : ∀A,B,C,f,g.
+injective A B f → injective B C g → injective A C (λx.g (f x)).
+/3/; qed.
+
+(* extensional equality *)
+
+definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
+λA.λP,Q.∀a.iff (P a) (Q a).
+
+definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
+λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
+
+definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
+λA,B.λf,g.∀a.f a = g a.
+
+notation " x \eqP y " non associative with precedence 45 
+for @{'eqP A $x $y}.
+
+interpretation "functional extentional equality" 
+'eqP A x y = (exteqP A x y).
+
+notation "x \eqR y" non associative with precedence 45 
+for @{'eqR ? ? x y}.
+
+interpretation "functional extentional equality" 
+'eqR A B R S = (exteqR A B R S).
+
+notation " f \eqF g " non associative with precedence 45
+for @{'eqF ? ? f g}.
+
+interpretation "functional extentional equality" 
+'eqF A B f g = (exteqF A B f g).
+
diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
new file mode 100644
index 000000000..c14cc60b4
--- /dev/null
+++ b/matita/matita/lib/basics/types.ma
@@ -0,0 +1,59 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_______________________________________________________________ *)
+
+include "basics/logic.ma".
+
+(* void *)
+inductive void : Type[0] ≝.
+
+(* unit *)
+inductive unit : Type[0] ≝ it: unit.
+
+(* Prod *)
+inductive Prod (A,B:Type[0]) : Type[0] ≝
+pair : A → B → Prod A B.
+
+interpretation "Pair construction" 'pair x y = (pair ? ? x y).
+
+interpretation "Product" 'product x y = (Prod x y).
+
+definition fst ≝ λA,B.λp:A × B.
+  match p with [pair a b ⇒ a]. 
+
+definition snd ≝ λA,B.λp:A × B.
+  match p with [pair a b ⇒ b].
+
+interpretation "pair pi1" 'pi1 = (fst ? ?).
+interpretation "pair pi2" 'pi2 = (snd ? ?).
+interpretation "pair pi1" 'pi1a x = (fst ? ? x).
+interpretation "pair pi2" 'pi2a x = (snd ? ? x).
+interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
+interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
+
+theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
+  p = 〈 \fst p, \snd p 〉.
+#A #B #p (cases p) // qed.
+
+(* sum *)
+inductive Sum (A,B:Type[0]) : Type[0] ≝
+  inl : A → Sum A B
+| inr : B → Sum A B.
+
+interpretation "Disjoint union" 'plus A B = (Sum A B).
+
+(* option *)
+inductive option (A:Type[0]) : Type[0] ≝
+   None : option A
+ | Some : A → option A.
+
+(* sigma *)
+inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
+  dp: ∀a:A.(f a)→Sig A f.
\ No newline at end of file
diff --git a/matita/matita/lib/hints_declaration.ma b/matita/matita/lib/hints_declaration.ma
new file mode 100644
index 000000000..bcbfed4f3
--- /dev/null
+++ b/matita/matita/lib/hints_declaration.ma
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* 
+
+Notation for hint declaration
+==============================
+
+The idea is to write a context, with abstraction first, then
+recursive calls (let-in) and finally the two equivalent terms.
+The context can be empty. Note the ; to begin the second part of
+the context (necessary even if the first part is empty). 
+
+ unification hint PREC \coloneq
+   ID : TY, ..., ID : TY
+   ; ID \equest T, ..., ID \equest T
+   \vdash T1 \equiv T2       
+
+With unidoce and some ASCII art it looks like the following:
+
+ unification hint PREC ≔ ID : TY, ..., ID : TY;
+    ID ≟ T, ..., ID ≟ T
+ (*---------------------*) ⊢
+         T1 ≡ T2       
+
+The order of premises is relevant, since they are processed in order
+(left to right).
+
+*)
+   
+(* it seems unbelivable, but it works! *)
+notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 19 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
+  with precedence 90
+  for @{ ${ fold right 
+               @{ ${ default 
+                    @{ ${ fold right 
+                        @{ 'hint_decl $Px $Py } 
+                        rec acc1 @{ let ( ${ident U} : ?) ≝ $V in $acc1} } }
+                    @{ 'hint_decl $Px $Py } 
+                 }
+               } 
+               rec acc @{ 
+                 ${ fold right @{ $acc } rec acc2 
+                      @{ ∀${ident x}:${ default @{ $T } @{ ? } }.$acc2 } } 
+               }
+       }}.
+
+include "basics/pts.ma".
+
+definition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.Prop.
+definition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.Prop.
+definition hint_declaration_Type2  ≝  λa,b:Type[2].Prop.
+definition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.Prop.
+definition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.Prop.
+definition hint_declaration_CProp2 ≝  λa,b:CProp[2].Prop.
+  
+interpretation "hint_decl_Type2"  'hint_decl a b = (hint_declaration_Type2 a b).
+interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
+interpretation "hint_decl_Type1"  'hint_decl a b = (hint_declaration_Type1 ? a b).
+interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b).
+interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
+interpretation "hint_decl_Type0"  'hint_decl a b = (hint_declaration_Type0 ? a b).
+
+(* Non uniform coercions support 
+record lock2 (S : Type[2]) (s : S) : Type[3] ≝ {
+  force2 : Type[2];
+  lift2  : force2
+}.
+
+record lock1 (S : Type[1]) (s : S) : Type[2] ≝ {
+  force1 : Type[1];
+  lift1  : force1
+}.
+
+coercion zzzlift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1 
+ on s : ? to force1 ???.
+
+coercion zzzlift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2
+ on s : ? to force2 ???.
+
+(* Example of a non uniform coercion declaration 
+   
+     Type[0]              setoid
+                >--->     
+     MR                   R  
+
+   provided MR = carr R
+
+unification hint 0 ≔ R : setoid;
+   MR ≟ carr R, 
+   lock ≟ mk_lock1 Type[0] MR setoid R 
+(* ---------------------------------------- *) ⊢ 
+   setoid ≡ force1 ? MR lock.
+
+*)
+*)
\ No newline at end of file
diff --git a/matita/matita/lib/root b/matita/matita/lib/root
new file mode 100644
index 000000000..c57405b94
--- /dev/null
+++ b/matita/matita/lib/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/