X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftotient.ma;h=ecbfce554460d6433a14d3f3516823d4dfc8a8b9;hb=2a31f145f58f7ba66b6445a9c8b31841054ef809;hp=a86986a81f743efd78b0dd004e38653c0788d601;hpb=d5afc8f8891d0020f5804eb2322fc0d1c8c60702;p=helm.git

diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma
index a86986a81..ecbfce554 100644
--- a/helm/software/matita/library/nat/totient.ma
+++ b/helm/software/matita/library/nat/totient.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/totient".
-
 include "nat/chinese_reminder.ma".
 include "nat/iteration2.ma".
 
@@ -33,7 +31,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.