X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Ftotient.ma;h=24c3920ed82571324c2977a7be798b492fbf43e7;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=7fc8d95ee15f9bd6f169a774166836087c4d1c00;hpb=65312e560c25b49336241762107e401e7f9c5c3c;p=helm.git

diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index 7fc8d95ee..24c3920ed 100644
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -31,22 +31,22 @@ qed.
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
 intro.
-apply nat_case n.
+apply (nat_case n).
 intro.simplify.intro.reflexivity.
-intros 2.apply nat_case m1.
+intros 2.apply (nat_case m1).
 rewrite < sym_times.
-rewrite < sym_times (totient O).
+rewrite < (sym_times (totient O)).
 simplify.intro.reflexivity.
 intros.
 unfold totient.
-apply count_times m m2 ? ? ? 
-(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)).
+apply (count_times m m2 ? ? ? 
+(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2))).
 intros.unfold cr_pair.
-apply le_to_lt_to_lt ? (pred ((S m)*(S m2))).
+apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))).
 unfold min.
 apply le_min_aux_r.
-change with (S (pred ((S m)*(S m2)))) \le ((S m)*(S m2)).
-apply nat_case ((S m)*(S m2)).apply le_n.
+change with ((S (pred ((S m)*(S m2)))) \le ((S m)*(S m2))).
+apply (nat_case ((S m)*(S m2))).apply le_n.
 intro.apply le_n.
 intros.
 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
@@ -64,4 +64,39 @@ intro.
 rewrite > eq_to_eqb_true.
 rewrite > eq_to_eqb_true.
 reflexivity.
-rewrite < H4.
\ No newline at end of file
+rewrite < H4.
+rewrite > sym_gcd.
+rewrite > gcd_mod.
+apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+rewrite < H5.
+rewrite > sym_gcd.
+rewrite > gcd_mod.
+apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+rewrite > sym_times.
+assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+intro.
+apply eqb_elim.
+intro.apply eqb_elim.
+intro.apply False_ind.
+apply H6.
+apply eq_gcd_times_SO.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+rewrite < gcd_mod.
+rewrite > H4.
+rewrite > sym_gcd.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+rewrite < gcd_mod.
+rewrite > H5.
+rewrite > sym_gcd.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+intro.reflexivity.
+intro.reflexivity.
+qed.
\ No newline at end of file