* Some simplifications to theorem in file totient1.ma.

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

diff --git a/matita/library/nat/gcd_properties1.ma b/matita/library/nat/gcd_properties1.ma
index 8687e2c1f7ececee716b5fdcf0efc1136e3b9313..bb8b9bb534881a1c019558c9212310bc669f2c72 100644 (file)
--- a/matita/library/nat/gcd_properties1.ma
+++ b/matita/library/nat/gcd_properties1.ma
@@ -18,145 +18,6 @@ include "nat/gcd.ma".
 
 (* this file contains some important properites of gcd in N *)
 
-(*it's a generalization of the existing theorem divides_gcd_aux (in which
-  c = 1), proved in file gcd.ma
- *)
-theorem divides_times_gcd_aux: \forall p,m,n,d,c. 
-O \lt c \to O < n \to n \le m \to n \le p \to
-d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n. 
-intro.
-elim p
-[ absurd (O < n)
-  [ assumption
-  | apply le_to_not_lt.
-    assumption
-  ]
-| simplify.
-  cut (n1 \divides m \lor n1 \ndivides m)
-  [ elim Hcut
-    [ rewrite > divides_to_divides_b_true
-      [ simplify.
-        assumption
-      | assumption
-      | assumption
-      ]
-    | rewrite > not_divides_to_divides_b_false
-      [ simplify.
-        apply H
-        [ assumption
-        | cut (O \lt m \mod n1 \lor O = m \mod n1)
-          [ elim Hcut1
-            [ assumption
-            | absurd (n1 \divides m)
-              [ apply mod_O_to_divides
-                [ assumption
-                | apply sym_eq.
-                  assumption
-                ]
-              | assumption
-              ]
-            ]
-          | apply le_to_or_lt_eq.
-            apply le_O_n
-          ]
-        | apply lt_to_le.
-          apply lt_mod_m_m.
-          assumption
-        | apply le_S_S_to_le.
-          apply (trans_le ? n1)
-          [ change with (m \mod n1 < n1).
-            apply lt_mod_m_m.
-            assumption
-          | assumption
-          ]
-        | assumption
-        | rewrite < times_mod
-          [ rewrite < (sym_times c m).
-            rewrite < (sym_times c n1).
-            apply divides_mod
-            [ rewrite > (S_pred c)
-              [ rewrite > (S_pred n1)
-                [ apply (lt_O_times_S_S)
-                | assumption
-                ]
-              | assumption
-              ]
-            | assumption
-            | assumption
-            ]
-          | assumption
-          | assumption
-          ]
-        ]
-      | assumption
-      | assumption
-      ]
-    ]
-  | apply (decidable_divides n1 m).
-    assumption
-  ]
-]
-qed.
-
-(*it's a generalization of the existing theorem divides_gcd_d (in which
-  c = 1), proved in file gcd.ma
- *)
-theorem divides_d_times_gcd: \forall m,n,d,c. 
-O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m. 
-intros.
-change with
-(d \divides c *
-match leb n m with
-  [ true \Rightarrow 
-    match n with 
-    [ O \Rightarrow m
-    | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
-  | false \Rightarrow 
-    match m with 
-    [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
-apply (leb_elim n m)
-[ apply (nat_case1 n)
-  [ simplify.
-    intros.
-    assumption
-  | intros.
-    change with (d \divides c*gcd_aux (S m1) m (S m1)).
-    apply divides_times_gcd_aux
-    [ assumption
-    | unfold lt.
-      apply le_S_S.
-      apply le_O_n
-    | assumption
-    | apply (le_n (S m1))
-    | assumption
-    | rewrite < H3.
-      assumption
-    ]
-  ]
-| apply (nat_case1 m)
-  [ simplify.
-    intros.
-    assumption
-  | intros.
-    change with (d \divides c * gcd_aux (S m1) n (S m1)).
-    apply divides_times_gcd_aux
-    [ unfold lt.
-      change with (O \lt c).
-      assumption
-    | apply lt_O_S
-    | apply lt_to_le.
-      apply not_le_to_lt.
-      assumption
-    | apply (le_n (S m1)).
-    | assumption
-    | rewrite < H3.
-      assumption
-    ]
-  ]
-]
-qed.
-
 (* an alternative characterization for gcd *)
 theorem gcd1: \forall a,b,c:nat.
 c \divides a \to c \divides b \to
@@ -245,14 +106,13 @@ O \lt m \to m \divides a \to m \divides b \to
 intros.
 apply (inj_times_r1 m H).
 rewrite > (sym_times m ((gcd a b)/m)).
-rewrite > (divides_to_times_div (gcd a b) m)
+rewrite > (divides_to_div m (gcd a b))
 [ rewrite < eq_gcd_times_times_times_gcd.
   rewrite > (sym_times m (a/m)).
   rewrite > (sym_times m (b/m)).
-  rewrite > (divides_to_times_div a m H H1).
-  rewrite > (divides_to_times_div b m H H2).
+  rewrite > (divides_to_div m a H1).
+  rewrite > (divides_to_div m b H2).
   reflexivity
-| assumption
 | apply divides_d_gcd;
     assumption
 ]
@@ -292,9 +152,8 @@ apply (nat_case1 a)
   [ cut (O \lt (gcd a b))
     [ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c)
       [ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)).
-        rewrite > (divides_to_times_div a (gcd a b))
+        rewrite > (divides_to_div (gcd a b) a)
         [ assumption      
-        | assumption
         | apply divides_gcd_n
         ]
       | rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %)
@@ -309,15 +168,13 @@ apply (nat_case1 a)
         apply (inj_times_r1 (gcd a b) Hcut1).
         rewrite < assoc_times.
         rewrite < sym_times in \vdash (? ? (? % ?) ?).
-        rewrite > (divides_to_times_div b (gcd a b))
+        rewrite > (divides_to_div (gcd a b) b)
         [ rewrite < assoc_times in \vdash (? ? ? %).
           rewrite < sym_times in \vdash (? ? ? (? % ?)).
-          rewrite > (divides_to_times_div a (gcd a b))
+          rewrite > (divides_to_div (gcd a b) a)
           [ assumption
-          | assumption
           | apply divides_gcd_n
           ]
-        | assumption
         | apply divides_gcd_m
         ]
       ]