* Some simplifications to theorem in file totient1.ma.

[helm.git] / matita / library / nat / primes.ma

diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma
index 45f520d087115bb5c5b7c105e569e6f2ce2efe1d..f7d6970063c4cf9b06a1e771c73b50c876bc1894 100644 (file)
--- a/matita/library/nat/primes.ma
+++ b/matita/library/nat/primes.ma
@@ -190,27 +190,51 @@ rewrite > H2.rewrite < H3.
 simplify.exact (not_le_Sn_n O).
 qed.
 
+
 (*divides and div*)
 
-theorem divides_to_times_div: \forall n,m:nat.
-O \lt m \to m \divides n \to (n / m) * m = n.
+theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
+intro.
+elim (le_to_or_lt_eq O n (le_O_n n))
+  [rewrite > plus_n_O.
+   rewrite < (divides_to_mod_O ? ? H H1).
+   apply sym_eq.
+   apply div_mod.
+   assumption
+  |elim H1.
+   generalize in match H2.
+   rewrite < H.
+   simplify.
+   intro.
+   rewrite > H3.
+   reflexivity
+  ]
+qed.
+
+theorem div_div: \forall n,d:nat. O < n \to divides d n \to 
+n/(n/d) = d.
 intros.
-rewrite > plus_n_O.
-apply sym_eq.
-cut (n \mod m = O)
-[ rewrite < Hcut.
-  apply div_mod.
-  assumption
-| apply divides_to_mod_O;
-    assumption.
-]
+apply (inj_times_l1 (n/d))
+  [apply (lt_times_n_to_lt d)
+    [apply (divides_to_lt_O ? ? H H1).
+    |rewrite > divides_to_div;assumption
+    ]
+  |rewrite > divides_to_div
+    [rewrite > sym_times.
+     rewrite > divides_to_div
+      [reflexivity
+      |assumption
+      ]
+    |apply (witness ? ? d).
+     apply sym_eq.
+     apply divides_to_div.
+     assumption
+    ]
+  ]
 qed.
 
-(*to remove hypotesis b > 0*)
 theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat.
 O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
-(*theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat.
-c \divides b \to a * (b /c) = (a*b)/c.*)
 intros.
 elim H1.
 rewrite > H2.
@@ -229,6 +253,7 @@ cut(O \lt c)
 ]
 qed.
 
+
 (* boolean divides *)
 definition divides_b : nat \to nat \to bool \def
 \lambda n,m :nat. (eqb (m \mod n) O).