* Some simplifications to theorem in file totient1.ma.

* Some theorems moved from file gcd_propreties1.ma to file gcd.ma.
* Some theorems moved from file dirichlet_product.ma to files div_and_mod.ma and primes.ma.

diff --git a/helm/software/matita/library/Z/dirichlet_product.ma b/helm/software/matita/library/Z/dirichlet_product.ma
index a1cc3d18e9fdc81a39070fce6e39782fdc722b67..edc2037618215b7a5f0bb5ddf07d1d142dab9039 100644 (file)
--- a/helm/software/matita/library/Z/dirichlet_product.ma
+++ b/helm/software/matita/library/Z/dirichlet_product.ma
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/Z/dirichlet_product".
 
+include "nat/primes.ma".
 include "Z/sigma_p.ma".
 include "Z/times.ma".
 
@@ -24,6 +25,7 @@ sigma_p (S n)
 
 (* da spostare *)
 
+(* spostati in div_and_mod.ma
 theorem mod_SO: \forall n:nat. mod n (S O) = O.
 intro.
 apply sym_eq.
@@ -40,7 +42,7 @@ rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
    apply times_n_SO
   |apply le_n
   ]
-qed.
+qed.*)
 
 theorem and_true: \forall a,b:bool. 
 andb a b =true \to a =true \land b= true.
@@ -88,7 +90,7 @@ elim (le_to_or_lt_eq O n (le_O_n n))
    assumption
   ]
 qed.
-
+(* spostato in primes.ma
 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))
@@ -105,8 +107,8 @@ elim (le_to_or_lt_eq O n (le_O_n n))
    rewrite > H3.
    reflexivity
   ]
-qed.
-
+qed.*)
+(* spostato in div_and_mod.ma
 theorem le_div: \forall n,m. O < n \to m/n \le m.
 intros.
 rewrite > (div_mod m n) in \vdash (? ? %)
@@ -118,7 +120,7 @@ rewrite > (div_mod m n) in \vdash (? ? %)
     ]
   |assumption
   ]
-qed.
+qed.*)
   
 theorem sigma_p2_eq: 
 \forall g: nat \to nat \to Z.
@@ -920,6 +922,7 @@ apply divides_to_divides_b_true1
   ]
 qed.
 
+(* spostato in primes.ma (non in div_and_mod.ma perche' serve il predicato divides)
 theorem div_div: \forall n,d:nat. O < n \to divides d n \to 
 n/(n/d) = d.
 intros.
@@ -941,7 +944,7 @@ apply (inj_times_l1 (n/d))
     ]
   ]
 qed.
-
+*)
 theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to 
 dirichlet_product f g n = dirichlet_product g f n.
 intros.

diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma
index 658b07b686eb5e6c23f02f3247c64f02f8f25381..f7f2883d590a8118ae6a39a8c348a75dcb2ff565 100644 (file)
--- a/helm/software/matita/library/nat/div_and_mod.ma
+++ b/helm/software/matita/library/nat/div_and_mod.ma
@@ -293,6 +293,38 @@ constructor 1.
 assumption.reflexivity.
 qed.
 
+theorem mod_SO: \forall n:nat. mod n (S O) = O.
+intro.
+apply sym_eq.
+apply le_n_O_to_eq.
+apply le_S_S_to_le.
+apply lt_mod_m_m.
+apply le_n.
+qed.
+
+theorem div_SO: \forall n:nat. div n (S O) = n.
+intro.
+rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
+  [rewrite > mod_SO.
+   rewrite < plus_n_O.
+   apply times_n_SO
+  |apply le_n
+  ]
+qed.
+
+theorem le_div: \forall n,m. O < n \to m/n \le m.
+intros.
+rewrite > (div_mod m n) in \vdash (? ? %)
+  [apply (trans_le ? (m/n*n))
+    [rewrite > times_n_SO in \vdash (? % ?).
+     apply le_times
+      [apply le_n|assumption]
+    |apply le_plus_n_r
+    ]
+  |assumption
+  ]
+qed.
+
 (* injectivity *)
 theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
 change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q).

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 0568536dcb0f6d4cbaef1b94c3feb53d79b17824..ded9d4843ac6cf3cb4da2b4f564568db2df2e02b 100644 (file)
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/nat/gcd".
 
 include "nat/primes.ma".
+include "nat/lt_arith.ma".
 
 let rec gcd_aux p m n: nat \def
 match divides_b n m with
@@ -163,42 +164,109 @@ intros.
 exact (proj1 ? ? (divides_gcd_nm n m)).
 qed.
 
+
+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.
+
+(*a particular case of the previous theorem (setting c=1)*)
 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 d \divides m \to d \divides n \to d \divides 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.
-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.
-apply divides_mod.assumption.assumption.assumption.
-assumption.assumption.
-apply (decidable_divides n1 m).assumption.
+intros.
+rewrite > (times_n_SO (gcd_aux p m n)).
+rewrite < (sym_times (S O)).
+apply (divides_times_gcd_aux)
+[ apply (lt_O_S O)
+| assumption
+| assumption
+| assumption
+| rewrite > (sym_times (S O)).
+  rewrite < (times_n_SO m).
+  assumption
+| rewrite > (sym_times (S O)).
+  rewrite < (times_n_SO n).
+  assumption
+]
 qed.
 
-theorem divides_d_gcd: \forall m,n,d. 
-d \divides m \to d \divides n \to d \divides gcd n m. 
+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.
-(*CSC: here simplify simplifies too much because of a redex in gcd *)
 change with
-(d \divides
+(d \divides c *
 match leb n m with
   [ true \Rightarrow 
     match n with 
@@ -208,20 +276,63 @@ match leb n m with
     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 gcd_aux (S m1) m (S m1)).
-apply divides_gcd_aux.
-unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
-rewrite < H2.assumption.
-apply (nat_case1 m).simplify.intros.assumption.
+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.
+
+(*a particular case of the previous theorem (setting c=1)*)
+theorem divides_d_gcd: \forall m,n,d. 
+d \divides m \to d \divides n \to d \divides gcd n m. 
 intros.
-change with (d \divides gcd_aux (S m1) n (S m1)).
-apply divides_gcd_aux.
-unfold lt.apply le_S_S.apply le_O_n.
-apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
-rewrite < H2.assumption.
+rewrite > (times_n_SO (gcd n m)).
+rewrite < (sym_times (S O)).
+apply (divides_d_times_gcd)
+[ apply (lt_O_S O)
+| rewrite > (sym_times (S O)).
+  rewrite < (times_n_SO m).
+  assumption
+| rewrite > (sym_times (S O)).
+  rewrite < (times_n_SO n).
+  assumption
+]
 qed.
 
 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to

diff --git a/helm/software/matita/library/nat/gcd_properties1.ma b/helm/software/matita/library/nat/gcd_properties1.ma
index 8687e2c1f7ececee716b5fdcf0efc1136e3b9313..bb8b9bb534881a1c019558c9212310bc669f2c72 100644 (file)
--- a/helm/software/matita/library/nat/gcd_properties1.ma
+++ b/helm/software/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
         ]
       ]

diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma
index 45f520d087115bb5c5b7c105e569e6f2ce2efe1d..f7d6970063c4cf9b06a1e771c73b50c876bc1894 100644 (file)
--- a/helm/software/matita/library/nat/primes.ma
+++ b/helm/software/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).

diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma
index 3d6b6fafcfbc1b5817732e3b2d09702b86ee250b..74018378a893875f6f5b159d3f3eb5aa48677b65 100644 (file)
--- a/helm/software/matita/library/nat/totient1.ma
+++ b/helm/software/matita/library/nat/totient1.ma
@@ -25,6 +25,7 @@ include "nat/gcd_properties1.ma".
    number n is equal to n
  *)
 
+(*simple auxiliary properties*)
 theorem eq_div_times_div_times: \forall a,b,c:nat.
 O \lt b \to b \divides a \to b \divides c \to
 a / b * c = a * (c/b).
@@ -47,15 +48,12 @@ theorem lt_O_to_divides_to_lt_O_div:
 O \lt b \to a \divides b \to O \lt (b/a).
 intros.
 apply (O_lt_times_to_O_lt ? a).
-rewrite > (divides_to_times_div b a)
-[ assumption
-| apply (divides_to_lt_O a b H H1)
-| assumption
-]
+rewrite > (divides_to_div a b); 
+  assumption.
 qed.
 
 (*tha main theorem*) 
-theorem sigma_p_Sn_divides_b_totient_n': \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n.
+theorem sigma_p_Sn_divides_b_totient_n: \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n.
 intros. 
 unfold totient.
 apply (trans_eq ? ? 
@@ -104,9 +102,8 @@ apply (trans_eq ? ?
           [ split
             [ apply divides_to_divides_b_true
               [ apply (O_lt_times_to_O_lt ? (gcd x n)).
-                rewrite > (divides_to_times_div n (gcd x n))
+                rewrite > (divides_to_div (gcd x n) n)
                 [ assumption
-                | assumption
                 | apply (divides_gcd_m)
                 ]
               | rewrite > sym_gcd.
@@ -119,13 +116,11 @@ apply (trans_eq ? ?
                 change with (x/(gcd x n) \lt n/(gcd x n)).
                 apply (lt_times_n_to_lt (gcd x n) ? ?)
                 [ assumption
-                | rewrite > (divides_to_times_div x (gcd x n))
-                  [ rewrite > (divides_to_times_div n (gcd x n))
+                | rewrite > (divides_to_div (gcd x n) x)
+                  [ rewrite > (divides_to_div (gcd x n) n)
                     [ assumption
-                    | assumption
                     | apply divides_gcd_m
                     ]
-                  | assumption
                   | apply divides_gcd_n
                   ]
                 ]
@@ -144,7 +139,7 @@ apply (trans_eq ? ?
               | apply divides_gcd_m 
               ]
             | rewrite > associative_times.
-              rewrite > (divides_to_times_div n (n/(gcd x n)))
+              rewrite > (divides_to_div (n/(gcd x n)) n)
               [ apply eq_div_times_div_times
                 [ assumption
                 | apply divides_gcd_n
@@ -161,29 +156,23 @@ apply (trans_eq ? ?
                 apply lt_O_gcd.
                 assumption.                
                 apply divides_gcd_n.*)
-              | apply lt_O_to_divides_to_lt_O_div
-                [ assumption
-                | apply divides_gcd_m 
-                ] 
               | apply (witness ? ? (gcd x n)).
-                rewrite > divides_to_times_div
+                rewrite > divides_to_div
                 [ reflexivity
-                | assumption
-                | apply divides_gcd_m
-                
+                | apply divides_gcd_m                
                 ]                
               ]
             ]  
           ]
         | apply (le_to_lt_to_lt ? n)
-          [ apply cic:/matita/Z/dirichlet_product/le_div.con.
+          [ apply le_div.
             assumption
           | change with ((S n) \le (S n)).
             apply le_n 
           ]
         ]
       | apply (le_to_lt_to_lt ? x)
-        [ apply cic:/matita/Z/dirichlet_product/le_div.con.
+        [ apply le_div.
           assumption   
         | apply (trans_lt ? n ?)
           [ assumption
@@ -206,7 +195,7 @@ apply (trans_eq ? ?
                 [ split
                   [ reflexivity
                   | rewrite > Hcut3.
-                    apply (cic:/matita/Z/dirichlet_product/div_div.con);
+                    apply (div_div);
                       assumption
                   ]               
                 | rewrite > Hcut3.
@@ -222,23 +211,21 @@ apply (trans_eq ? ?
                   | apply divides_n_n
                   ]
                 ]
-              | rewrite < (divides_to_times_div n i) in \vdash (? ? %)
+              | rewrite < (divides_to_div i n) in \vdash (? ? %)
                 [ rewrite > sym_times.
                   apply (lt_times_r1)
                   [ apply lt_O_to_divides_to_lt_O_div; (*n/i 3*)
                       assumption
                   | assumption
                   ]
-                | apply (divides_to_lt_O i n); assumption
                 | assumption
                 ]               
               ]
-            | rewrite < (divides_to_times_div n i) in \vdash (? ? (? ? %) ?)
+            | rewrite < (divides_to_div i n) in \vdash (? ? (? ? %) ?)
               [ rewrite > (sym_times j).
                 rewrite > times_n_SO in \vdash (? ? ? %).
                 rewrite < Hcut2.
-                apply eq_gcd_times_times_times_gcd.                
-              | apply (divides_to_lt_O i n); assumption
+                apply eq_gcd_times_times_times_gcd                
               | assumption
               ]
             ]