Unfinished proof commented out.

diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index df863fa04f7746f86104ecaea9a9f223ae0d41d4..6715fe854993ebce6ca7b668606ed9ab64c97f42 100644 (file)
--- 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.
+*)