X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev.ma;h=2a3695e8e99c401322e4491248d62c6442c4d7ef;hb=8da75ffeb862139e8607c5a3a3aa782458da82cb;hp=fa935be03784040f76892ff02fb0628b6e2ee687;hpb=2abee6f6b5f1cf989224c64e6ab9091624a34248;p=helm.git

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index fa935be03..2a3695e8e 100644
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -22,6 +22,7 @@ include "nat/factorial2.ma".
 definition prim: nat \to nat \def
 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
 
+(* This is chebishev psi funcion *)
 definition A: nat \to nat \def
 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
 
@@ -79,6 +80,7 @@ elim (le_to_or_lt_eq ? ? (le_O_n n))
   ]
 qed.
 
+(* an equivalent formulation for psi *)
 definition A': nat \to nat \def
 \lambda n. pi_p (S n) primeb 
   (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
@@ -327,7 +329,8 @@ intro.elim q
     ]
   ]
 qed.
-    
+
+(* factorization of n into primes *)
 theorem pi_p_primeb_divides_b: \forall n. O < n \to 
 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
 intros.
@@ -505,6 +508,7 @@ apply eq_pi_p1
   ]
 qed.
 
+(* the factorial function *)
 theorem eq_fact_pi_p:\forall n. fact n = 
 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
 intro.elim n
@@ -590,6 +594,7 @@ apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
   ]
 qed.              
 
+(* still another characterization of the factorial *)
 theorem fact_pi_p: \forall n. fact n =
 pi_p (S n) primeb 
   (\lambda p.(pi_p (log p n) 
@@ -1161,8 +1166,7 @@ rewrite > eq_A_SSO_n
            assumption
           |cut (i\sup(S i1)≤(S(S O))*n)
             [apply div_mod_spec_intro
-              [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
-               apply lt_plus_to_lt_minus
+              [apply lt_plus_to_lt_minus
                 [assumption
                 |simplify in ⊢ (? % ?).
                  rewrite < plus_n_O.