From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 12 Oct 2007 09:59:54 +0000 (+0000)
Subject: Reorganization of the library.
X-Git-Tag: 0.4.95@7852~138
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b7f77f52fa66ace34da12dd7e5efcae05be6cbe5;p=helm.git

Reorganization of the library.
---

diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma
index 9ab53fd74..6ad389346 100644
--- a/matita/library/nat/le_arith.ma
+++ b/matita/library/nat/le_arith.ma
@@ -20,9 +20,10 @@ include "nat/orders.ma".
 (* plus *)
 theorem monotonic_le_plus_r: 
 \forall n:nat.monotonic nat le (\lambda m.n + m).
-simplify.intros.elim n.
-simplify.assumption.
-simplify.apply le_S_S.assumption.
+simplify.intros.elim n
+  [simplify.assumption.
+  |simplify.apply le_S_S.assumption
+  ]
 qed.
 
 theorem le_plus_r: \forall p,n,m:nat. n \le m \to p + n \le p + m
@@ -41,9 +42,21 @@ theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \le n2  \to m1 \le m2 
 \to n1 + m1 \le n2 + m2.
 intros.
+(**
+auto.
+*)
+apply (transitive_le (plus n1 m1) (plus n1 m2) (plus n2 m2) ? ?);
+  [apply (monotonic_le_plus_r n1 m1 m2 ?).
+   apply (H1).
+  |apply (monotonic_le_plus_l m2 n1 n2 ?).
+   apply (H).
+  ]
+(* end auto($Revision$) proof: TIME=0.61 SIZE=100 DEPTH=100 *)
+(*
 apply (trans_le ? (n2 + m1)).
 apply le_plus_l.assumption.
 apply le_plus_r.assumption.
+*)
 qed.
 
 theorem le_plus_n :\forall n,m:nat. m \le n + m.
diff --git a/matita/library/nat/lt_arith.ma b/matita/library/nat/lt_arith.ma
index cce6626a0..a568ca408 100644
--- a/matita/library/nat/lt_arith.ma
+++ b/matita/library/nat/lt_arith.ma
@@ -262,6 +262,26 @@ apply lt_to_not_eq.assumption.
 intro.reflexivity.
 qed.
 
+(* times and plus *)
+theorem lt_times_plus_times: \forall a,b,n,m:nat. 
+a < n \to b < m \to a*m + b < n*m.
+intros 3.
+apply (nat_case n)
+  [intros.apply False_ind.apply (not_le_Sn_O ? H)
+  |intros.simplify.
+   rewrite < sym_plus.
+   unfold.
+   change with (S b+a*m1 \leq m1+m*m1).
+   apply le_plus
+    [assumption
+    |apply le_times
+      [apply le_S_S_to_le.assumption
+      |apply le_n
+      ]
+    ]
+  ]
+qed.
+
 (* div *) 
 
 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m. 
diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma
index f7d697006..6885a9847 100644
--- a/matita/library/nat/primes.ma
+++ b/matita/library/nat/primes.ma
@@ -211,6 +211,14 @@ elim (le_to_or_lt_eq O n (le_O_n n))
   ]
 qed.
 
+theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
+intros.
+apply (witness ? ? d).
+apply sym_eq.
+apply divides_to_div.
+assumption.
+qed.
+
 theorem div_div: \forall n,d:nat. O < n \to divides d n \to 
 n/(n/d) = d.
 intros.
@@ -287,7 +295,8 @@ intros 2.apply (nat_case n)
   [apply (nat_case m)
     [intro.apply divides_n_n
     |simplify.intros.apply False_ind.
-     apply not_eq_true_false.apply sym_eq.assumption
+     apply not_eq_true_false.apply sym_eq.
+     assumption
     ]
   |intros.
    apply divides_b_true_to_divides1
@@ -345,6 +354,22 @@ elim (divides_b n m).reflexivity.
 absurd (n \divides m).assumption.assumption.
 qed.
 
+theorem divides_to_divides_b_true1 : \forall n,m:nat.
+O < m \to n \divides m \to divides_b n m = true.
+intro.
+elim (le_to_or_lt_eq O n (le_O_n n))
+  [apply divides_to_divides_b_true
+    [assumption|assumption]
+  |apply False_ind.
+   rewrite < H in H2.
+   elim H2.
+   simplify in H3.
+   apply (not_le_Sn_O O).
+   rewrite > H3 in H1.
+   assumption
+  ]
+qed.
+
 theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
 \lnot(n \divides m) \to (divides_b n m) = false.
 intros.
@@ -357,6 +382,18 @@ absurd (n \divides m).assumption.assumption.
 reflexivity.
 qed.
 
+theorem divides_b_div_true: 
+\forall d,n. O < n \to 
+  divides_b d n = true \to divides_b (n/d) n = true.
+intros.
+apply divides_to_divides_b_true1
+  [assumption
+  |apply divides_div.
+   apply divides_b_true_to_divides.
+   assumption
+  ]
+qed.
+
 theorem divides_b_true_to_lt_O: \forall n,m. O < n \to divides_b m n = true \to O < m.
 intros.
 elim (le_to_or_lt_eq ? ? (le_O_n m))
diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma
index a86986a81..9933490a2 100644
--- a/matita/library/nat/totient.ma
+++ b/matita/library/nat/totient.ma
@@ -33,7 +33,9 @@ include "nat/iteration2.ma".
 definition totient : nat \to nat \def
 \lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O).
 
-                                        
+lemma totient1: totient (S(S(S(S(S(S O)))))) = ?.
+[|simplify.
+                                
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
 intros.