From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 2 Nov 2005 18:48:52 +0000 (+0000)
Subject: Unfinished proof commented out.
X-Git-Tag: V_0_7_2_3~153
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f11e6250691c73a64315052bb910e23c87aea8a8;p=helm.git

Unfinished proof commented out.
---

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.
+*)