From f11e6250691c73a64315052bb910e23c87aea8a8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 2 Nov 2005 18:48:52 +0000 Subject: [PATCH] Unfinished proof commented out. --- helm/matita/library/nat/totient.ma | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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. +*) -- 2.39.2