X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftotient1.ma;h=e12c85adbe5e171962595ca9f4343d4b36686c81;hb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;hp=74018378a893875f6f5b159d3f3eb5aa48677b65;hpb=db9c252cc8adb9243892203805b203bafe486bfc;p=helm.git

diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma
index 74018378a..e12c85adb 100644
--- a/helm/software/matita/library/nat/totient1.ma
+++ b/helm/software/matita/library/nat/totient1.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/totient1".
-
 include "nat/totient.ma".
 include "nat/iteration2.ma".
 include "nat/gcd_properties1.ma".
@@ -25,24 +23,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).
-intros.
-elim H1.
-elim H2.
-rewrite > H3.
-rewrite > H4.    
-rewrite > (sym_times) in \vdash (? ? ? (? ? (? % ?))).
-rewrite > (sym_times) in \vdash (? ? (? (? % ?) ?) ?).
-rewrite > (lt_O_to_div_times ? ? H).
-rewrite > (lt_O_to_div_times ? ? H) in \vdash (? ? ? (? ? %)).
-rewrite > (sym_times b n2).
-rewrite > assoc_times.
-reflexivity.
-qed.
-    
+(*simple auxiliary properties*)   
 theorem lt_O_to_divides_to_lt_O_div:
 \forall a,b:nat.
 O \lt b \to a \divides b \to O \lt (b/a).
@@ -124,7 +105,7 @@ apply (trans_eq ? ?
                   | apply divides_gcd_n
                   ]
                 ]
-              | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
+              | apply eq_to_eqb_true.
                 rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
                 [ apply (div_n_n (gcd x n) Hcut)
                 | assumption
@@ -140,22 +121,24 @@ apply (trans_eq ? ?
               ]
             | rewrite > associative_times.
               rewrite > (divides_to_div (n/(gcd x n)) n)
-              [ apply eq_div_times_div_times
-                [ assumption
-                | apply divides_gcd_n
+              [ rewrite > sym_times.
+                rewrite > (divides_to_eq_times_div_div_times x)
+                [ apply (inj_times_l1 (gcd x n) Hcut).
+                  rewrite > (divides_to_div (gcd x n) (x * n))
+                  [ rewrite > assoc_times.
+                    rewrite > (divides_to_div (gcd x n) x)
+                    [ apply sym_times
+                    | apply divides_gcd_n
+                    ]
+                  | apply (trans_divides ? x)
+                    [ apply divides_gcd_n
+                    | apply (witness ? ? n).
+                      reflexivity
+                    ]
+                  ]
+                | assumption
                 | apply divides_gcd_m
-                ]
-                (*rewrite > sym_times.
-                rewrite > (divides_to_eq_times_div_div_times n).
-                rewrite > (divides_to_eq_times_div_div_times x).
-                rewrite > (sym_times n x).
-                reflexivity. 
-                assumption.
-                apply divides_gcd_m.
-                apply (divides_to_lt_O (gcd x n)).
-                apply lt_O_gcd.
-                assumption.                
-                apply divides_gcd_n.*)
+                ]              
               | apply (witness ? ? (gcd x n)).
                 rewrite > divides_to_div
                 [ reflexivity
@@ -203,10 +186,10 @@ apply (trans_eq ? ?
                   [ rewrite > div_n_n  
                     [ apply sym_eq.
                       apply times_n_SO.
-                    | apply lt_O_to_divides_to_lt_O_div; (*n/i 1*)
+                    | apply lt_O_to_divides_to_lt_O_div;
                         assumption
                     ]
-                  | apply lt_O_to_divides_to_lt_O_div; (*n/i 2*)
+                  | apply lt_O_to_divides_to_lt_O_div; 
                       assumption
                   | apply divides_n_n
                   ]
@@ -214,7 +197,7 @@ apply (trans_eq ? ?
               | 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*)
+                  [ apply lt_O_to_divides_to_lt_O_div;
                       assumption
                   | assumption
                   ]