X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftotient.ma;h=9933490a2dda03f20da09be3124dee5919ec3d8e;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=03e2587a8f02b1bc17eb3f3e8d0a8f932ad5417c;hpb=21d7aa4df8d5d4bfe1073720ea4f9410e9cec879;p=helm.git

diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma
index 03e2587a8..9933490a2 100644
--- a/helm/software/matita/library/nat/totient.ma
+++ b/helm/software/matita/library/nat/totient.ma
@@ -24,7 +24,7 @@ include "nat/iteration2.ma".
     phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1.
    (so this definition considers the values i=1,2,...,n)
   
-  sigma_p doesn't work ok the value n (but the first value it works on is (pred n))
+  sigma_p doesn't work on the value n (but the first value it works on is (pred n))
   but works also on 0. That's not a problem, in fact
    - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1. 
    - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1. 
@@ -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.
@@ -134,4 +136,4 @@ apply (nat_case1 n)
        ]
      ]
    ]
-qed.
\ No newline at end of file
+qed.