Bertrand's conjecture (weak), some work in progress

[helm.git] / helm / software / matita / library / nat / totient.ma

diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma
index a86986a81f743efd78b0dd004e38653c0788d601..9933490a2dda03f20da09be3124dee5919ec3d8e 100644 (file)
--- a/helm/software/matita/library/nat/totient.ma
+++ b/helm/software/matita/library/nat/totient.ma
@@ -33,7 +33,9 @@ include "nat/iteration2.ma".
 definition totient : nat \to nat \def
 \lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O).
 
-                                        
+lemma totient1: totient (S(S(S(S(S(S O)))))) = ?.
+[|simplify.
+                                
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
 intros.