X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Ftotient.ma;fp=helm%2Fmatita%2Flibrary%2Fnat%2Ftotient.ma;h=ff425772cd276d31b239c15bb35d5f5e6345ef50;hb=cca04138889cd0dbafb669a5c3fd8abe424d699e;hp=6715fe854993ebce6ca7b668606ed9ab64c97f42;hpb=82d56e6d22560ffb111c63cfdf0e200c8fa6fd3d;p=helm.git

diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index 6715fe854..ff425772c 100644
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -28,7 +28,6 @@ theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
 reflexivity.
 qed.
 
-(*
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
 intro.
@@ -66,4 +65,38 @@ rewrite > eq_to_eqb_true.
 rewrite > eq_to_eqb_true.
 reflexivity.
 rewrite < H4.
-*)
+rewrite > sym_gcd.
+rewrite > gcd_mod.
+apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
+simplify.apply le_S_S.apply le_O_n.
+simplify.apply le_S_S.apply le_O_n.
+assumption.
+simplify.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)).
+simplify.apply le_S_S.apply le_O_n.
+simplify.apply le_S_S.apply le_O_n.
+rewrite > sym_times.
+assumption.
+simplify.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.
+simplify.apply le_S_S.apply le_O_n.
+simplify.apply le_S_S.apply le_O_n.
+rewrite < gcd_mod.
+rewrite > H4.
+rewrite > sym_gcd.assumption.
+simplify.apply le_S_S.apply le_O_n.
+rewrite < gcd_mod.
+rewrite > H5.
+rewrite > sym_gcd.assumption.
+simplify.apply le_S_S.apply le_O_n.
+intro.reflexivity.
+intro.reflexivity.
+qed.
\ No newline at end of file