Nuova dimostrazione riflessiva di le_to_Bertrand.

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

diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma
index 211df69d0fa0d9941a9dcf14bebca51e1812ffda..752e89b9d02fec375326cd8d8df46b577daaef93 100644 (file)
--- a/helm/software/matita/library/nat/iteration2.ma
+++ b/helm/software/matita/library/nat/iteration2.ma
@@ -12,14 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/iteration2".
-
 include "nat/primes.ma".
 include "nat/ord.ma".
 include "nat/generic_iter_p.ma".
 include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
 
-
 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
 definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
 \lambda n, p, g. (iter_p_gen n p nat g O plus).