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=6715fe854993ebce6ca7b668606ed9ab64c97f42;hb=f11e6250691c73a64315052bb910e23c87aea8a8;hp=df863fa04f7746f86104ecaea9a9f223ae0d41d4;hpb=69dc6031c9e0574fa7a74ced74deeb7f9ec5695b;p=helm.git

diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index df863fa04..6715fe854 100644
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -28,6 +28,7 @@ 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.
@@ -64,4 +65,5 @@ intro.
 rewrite > eq_to_eqb_true.
 rewrite > eq_to_eqb_true.
 reflexivity.
-rewrite < H4.
\ No newline at end of file
+rewrite < H4.
+*)