]> matita.cs.unibo.it Git - helm.git/commitdiff
Complete proof of Bertrand for n >= 256.
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 18 Feb 2008 08:56:40 +0000 (08:56 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 18 Feb 2008 08:56:40 +0000 (08:56 +0000)
Removed the baseuri form all files in nat.

40 files changed:
helm/software/matita/library/nat/bertrand.ma
helm/software/matita/library/nat/binomial.ma
helm/software/matita/library/nat/chebyshev_teta.ma
helm/software/matita/library/nat/chebyshev_thm.ma
helm/software/matita/library/nat/chinese_reminder.ma
helm/software/matita/library/nat/compare.ma
helm/software/matita/library/nat/congruence.ma
helm/software/matita/library/nat/count.ma
helm/software/matita/library/nat/div_and_mod.ma
helm/software/matita/library/nat/div_and_mod_diseq.ma
helm/software/matita/library/nat/euler_theorem.ma
helm/software/matita/library/nat/exp.ma
helm/software/matita/library/nat/factorial.ma
helm/software/matita/library/nat/factorial2.ma
helm/software/matita/library/nat/factorization.ma
helm/software/matita/library/nat/fermat_little_theorem.ma
helm/software/matita/library/nat/gcd.ma
helm/software/matita/library/nat/generic_iter_p.ma
helm/software/matita/library/nat/iteration2.ma
helm/software/matita/library/nat/le_arith.ma
helm/software/matita/library/nat/log.ma
helm/software/matita/library/nat/lt_arith.ma
helm/software/matita/library/nat/map_iter_p.ma
helm/software/matita/library/nat/minimization.ma
helm/software/matita/library/nat/minus.ma
helm/software/matita/library/nat/nat.ma
helm/software/matita/library/nat/neper.ma
helm/software/matita/library/nat/nth_prime.ma
helm/software/matita/library/nat/ord.ma
helm/software/matita/library/nat/orders.ma
helm/software/matita/library/nat/permutation.ma
helm/software/matita/library/nat/pi_p.ma
helm/software/matita/library/nat/plus.ma
helm/software/matita/library/nat/primes.ma
helm/software/matita/library/nat/relevant_equations.ma
helm/software/matita/library/nat/sigma_and_pi.ma
helm/software/matita/library/nat/sqrt.ma
helm/software/matita/library/nat/times.ma
helm/software/matita/library/nat/totient.ma
helm/software/matita/library/nat/totient1.ma

index f014b0eccc15ba92cc7b5170fb617fa6496c41e2..20302e876f1ba02bbe81fde6b2f39a45506bad96 100644 (file)
 include "nat/sqrt.ma".
 include "nat/chebyshev_teta.ma".
 include "nat/chebyshev.ma".
+include "nat/o.ma".
+
+definition bertrand \def \lambda n.
+\exists p.n < p \land p \le 2*n \land (prime p).
 
 definition not_bertrand \def \lambda n.
 \forall p.n < p \to p \le 2*n \to \not (prime p).
 
+lemma not_not_bertrand_to_bertrand1: \forall n.
+\lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
+(\forall p.x < p \to p \le 2*n \to \not (prime p))
+\to \exists p.n < p \land p \le  x \land (prime p).
+intros 4.elim H1
+  [apply False_ind.apply H.assumption
+  |apply (bool_elim ? (primeb (S n1)));intro
+    [apply (ex_intro ? ? (S n1)).
+     split
+      [split
+        [apply le_S_S.assumption
+        |apply le_n
+        ]
+      |apply primeb_true_to_prime.assumption
+      ]
+    |elim H3
+      [elim H7.clear H7.
+       elim H8.clear H8.
+       apply (ex_intro ? ? a). 
+       split
+        [split
+          [assumption
+          |apply le_S.assumption
+          ]
+        |assumption
+        ]
+      |apply lt_to_le.assumption
+      |elim (le_to_or_lt_eq ? ? H7)
+        [apply H5;assumption
+        |rewrite < H9.
+         apply primeb_false_to_not_prime.
+         assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+  
+theorem not_not_bertrand_to_bertrand: \forall n.
+\lnot (not_bertrand n) \to bertrand n.
+unfold bertrand.intros.
+apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
+  [assumption
+  |apply le_times_n.apply le_n_Sn
+  |apply le_n
+  |intros.apply False_ind.
+   apply (lt_to_not_le ? ? H1 H2)
+  ]
+qed.
+  
 (* not used
 theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to 
 divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
@@ -511,8 +565,203 @@ rewrite < (eq_log_exp 2)
   ]
 qed.
 
-(*
-theorem tech: \forall n. 2*(3*(S(log 2 (2*n)))/4) < sqrt (2*n) \to
-(sqrt(2*n)/2)*S(log 2 (2*n)) < 2*n / 3.
+theorem tech1: \forall a,b,c,d.O < b \to O < d \to
+(a/b)*(c/d) \le (a*c)/(b*d).
+intros.
+apply le_times_to_le_div
+  [rewrite > (times_n_O O).
+   apply lt_times;assumption
+  |rewrite > assoc_times.
+   rewrite < assoc_times in ⊢ (? (? ? %) ?).
+   rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
+   rewrite > assoc_times.
+   rewrite < assoc_times.
+   apply le_times;
+   rewrite > sym_times;apply le_times_div_m_m;assumption
+  ]
+qed.
+
+theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
+(sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
+intros.
+cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
+  [rewrite > sym_times.
+   apply le_times_to_le_div
+    [apply lt_O_S
+    |rewrite < assoc_times.
+     apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
+      [apply le_times_l.assumption
+      |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
+        [apply le_times_div_div_times.
+         apply lt_O_S
+        |rewrite > assoc_times.
+         rewrite > sym_times.
+         rewrite > lt_O_to_div_times.
+         apply leq_sqrt_n.
+         apply lt_O_S
+        ]
+      ]
+    ]
+  |change in ⊢ (? (? % ?) ?) with (2*2).
+   rewrite > assoc_times.
+   apply le_times_r.
+   assumption
+  ]
+qed.
+
+theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to 
+n/(S m) < n/m.
+intros.
+apply lt_times_to_lt_div.
+apply (lt_to_le_to_lt ? (S(n/m)*m))
+  [apply lt_div_S.assumption
+  |rewrite > sym_times in ⊢ (? ? %). simplify.
+   rewrite > sym_times in ⊢ (? ? (? ? %)).
+   apply le_plus_l.
+   apply le_times_to_le_div
+    [assumption
+    |rewrite < exp_SSO.
+     assumption
+    ]
+  ]
+qed.
+
+theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
+intros.
+rewrite > exp_SSO.
+rewrite > distr_times_plus.
+rewrite > times_plus_l.
+rewrite < exp_SSO.
+rewrite > assoc_plus.
+rewrite > assoc_plus.
+apply eq_f.
+rewrite > times_plus_l.
+rewrite < exp_SSO.
+rewrite < assoc_plus.
+rewrite < sym_times.
+rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
+rewrite > assoc_times.
+apply eq_f2;reflexivity.
+qed.
+
+theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
 intros.
- *)                
+lapply (le_log 2 ? ? (le_n ?) H) as H1.
+rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
+rewrite > log_exp
+  [rewrite > sym_plus.
+   rewrite > plus_n_Sm.
+   unfold sqrt.
+   apply f_m_to_le_max
+    [apply le_times_r.
+     apply (trans_le ? (2*log 2 n))
+      [rewrite < times_SSO_n.
+       apply le_plus_r.
+       apply (trans_le ? 8)
+        [apply leb_true_to_le.reflexivity
+        |rewrite < (eq_log_exp 2)
+          [assumption
+          |apply le_n
+          ]
+        ]
+      |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
+       apply le_times_SSO_n_exp_SSO_n.
+       apply (lt_to_le_to_lt ? ? ? ? H).
+       apply leb_true_to_le.reflexivity
+      ]
+    |apply le_to_leb_true.
+     rewrite > assoc_times.
+     apply le_times_r.
+     rewrite > sym_times.
+     rewrite > assoc_times.
+     rewrite < exp_SSO.
+     rewrite > exp_plus_SSO.
+     rewrite > distr_times_plus.
+     rewrite > distr_times_plus.
+     rewrite > assoc_plus.
+     apply (trans_le ? (4*exp (log 2 n) 2))
+      [change in ⊢ (? ? (? % ?)) with (2*2).
+       rewrite > assoc_times in ⊢ (? ? %).
+       rewrite < times_SSO_n in ⊢ (? ? %).
+       apply le_plus_r.
+       rewrite < times_SSO_n in ⊢ (? ? %).
+       apply le_plus
+        [rewrite > sym_times in ⊢ (? (? ? %) ?).
+         rewrite < assoc_times.
+         rewrite < assoc_times.
+         change in ⊢ (? (? % ?) ?) with 8.
+         rewrite > exp_SSO.
+         apply le_times_l.
+         (* strange things here *)
+         rewrite < (eq_log_exp 2)
+          [assumption
+          |apply le_n
+          ]
+        |apply (trans_le ? (log 2 n))
+          [change in ⊢ (? % ?) with 8.
+           rewrite < (eq_log_exp 2)
+            [assumption
+            |apply le_n
+            ]
+          |rewrite > exp_n_SO in ⊢ (? % ?).
+           apply le_exp
+            [apply lt_O_log
+              [apply (lt_to_le_to_lt ? ? ? ? H).
+               apply leb_true_to_le.reflexivity
+              |apply (lt_to_le_to_lt ? ? ? ? H).
+               apply leb_true_to_le.reflexivity
+              ]
+            |apply le_n_Sn
+            ]
+          ]
+        ]
+      |change in ⊢ (? (? % ?) ?) with (exp 2 2).
+       apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
+        [apply le_times_exp_n_SSO_exp_SSO_n
+          [apply le_n
+          |change in ⊢ (? % ?) with 8.
+           rewrite < (eq_log_exp 2)
+            [assumption
+            |apply le_n
+            ]
+          ]
+        |apply (lt_to_le_to_lt ? ? ? ? H).
+         apply leb_true_to_le.reflexivity
+        ]
+      ]
+    ]
+  |apply le_n
+  |apply (lt_to_le_to_lt ? ? ? ? H).
+   apply leb_true_to_le.reflexivity
+  ]
+qed.
+      
+theorem le_to_bertrand:
+\forall n. (exp 2 8) \le n \to bertrand n.
+intros.
+apply not_not_bertrand_to_bertrand.unfold.intro.
+absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
+  [apply not_bertrand_to_le2
+    [apply (trans_le ? ? ? ? H). 
+     apply le_exp
+      [apply lt_O_S
+      |apply le_n_Sn
+      ]
+    |assumption
+    ]
+  |apply lt_to_not_le.
+   apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
+    [apply tech.apply tech3.assumption
+    |apply lt_O_S
+    |apply (trans_le ? (2*exp 2 8))
+      [apply leb_true_to_le.reflexivity
+      |apply le_times_r.assumption
+      ]
+    ]
+  ]
+qed.
+
+(* test 
+theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
+reflexivity.
+*)
index e7d58039a34baa3338a98f4c37c8ca459da2a49f..83ef0acbb99d54f43ec260f16dc60447966be230 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/binomial".
-
 include "nat/iteration2.ma".
 include "nat/factorial2.ma".
 
index 4c839892ade4ac32d696a817b623d96afc48ad51..1765b38072626e02bd6593da9f31654ac0c36d22 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/chebyshev_teta".
-
 include "nat/binomial.ma".
 include "nat/pi_p.ma".
 
index 248c9e3c67e041649752ac3f7262a7a789546c49..e90b22d9dfaf42d1eec8f2ce2060e3ff3b96a09d 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/chebyshev_thm/".
-
 include "nat/neper.ma".
 
 definition C \def \lambda n.pi_p (S n) primeb 
index 766b85f715324398d2cde65bddf9c96f3c8da90c..2bf3bc59e0d95c00510e827371b9eac04a453d1e 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/chinese_reminder".
-
 include "nat/exp.ma".
 include "nat/gcd.ma".
 include "nat/permutation.ma".
index b002d78cccdedd6ad690ffeea67aaa0402c14288..dd9589e7bfab7d75cf8b33d60c0c60d22e34d259 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/compare".
-
 include "datatypes/bool.ma".
 include "datatypes/compare.ma".
 include "nat/orders.ma".
index f418c1b8578a0a7de9e983a96c7291fd28fc73c4..753745d4540d23f1378fcd3f4ac9cbc2791f14e0 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/congruence".
-
 include "nat/relevant_equations.ma".
 include "nat/primes.ma".
 
index 2abcf25c3b1f43245c61bd8d7d046c663b1a259d..6b5dbbe660f4b23a9253a55e90832552ccae2fba 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/count".
-
 include "nat/relevant_equations.ma".
 include "nat/sigma_and_pi.ma".
 include "nat/permutation.ma".
index 523f7431403a14071e2154d661eb9f22ef552332..538515a8cc806003287340ef9d1299b4625a17a0 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/div_and_mod".
-
 include "datatypes/constructors.ma".
 include "nat/minus.ma".
 
-
 let rec mod_aux p m n: nat \def
 match (leb m n) with
 [ true \Rightarrow m
index 299897a38ce7222d93e9114a84ff51e8dc815d60..464998223bcdd3e8ac23790628504b8261f16152 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/div_and_mod_diseq".
-
 include "nat/lt_arith.ma".
 
 (* the proof that 
index 1e5988b35de64d1a9eba560dadd53e6929e98f15..9396d444ed4b5a93db0e074e200c451f082cf5aa 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/euler_theorem".
-
 include "nat/map_iter_p.ma".
 include "nat/totient.ma".
 
index 52793cb5a77b21d853ff56cac6868ff4c9e24905..c9f2c6984ee6d31aeb1ddc8ab9b96b936b19a9e0 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/exp".
-
 include "nat/div_and_mod.ma".
 include "nat/lt_arith.ma".
 
index 14217bbcbdee58a7dba618d68642da3eb315d37c..58220cb0cbcdbeedd773fb9d51cd9292da849882 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/factorial".
-
 include "nat/le_arith.ma".
 
 let rec fact n \def
index 6215d6657892ab39eb0233763885657f35796725..bcd228d0801a12f197312637ef7515236b4ba511 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/factorial2".
-
 include "nat/exp.ma".
 include "nat/factorial.ma".
 
index 8c50d1d7db1e5612e160776b39a59e55ab21fece..1ca684aed0692c05874db9dd9c1a5ca0174d3739 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/factorization".
-
 include "nat/ord.ma".
 
 (* the following factorization algorithm looks for the largest prime
index f7953346a35f8affd74864ff62e9c02c730176b8..1dc6669cbc4f8cf9f70b7c84b4a13ebbf8c19334 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/fermat_little_theorem".
-
 include "nat/exp.ma".
 include "nat/gcd.ma".
 include "nat/permutation.ma".
index 0baa86e3c28b43cfcddd5a8e0aa8f8a69af35685..3db29f622fb95a5e096cb46744928c97bcef9f39 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/gcd".
-
 include "nat/primes.ma".
 include "nat/lt_arith.ma".
 
index f89c32f870c6f4dfe26fd4406ce8a7079a3ea39f..5f15bddc93e86a452497614bae6fc236d1ebf9a7 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/generic_iter_p".
-
 include "nat/div_and_mod_diseq.ma".
 include "nat/primes.ma".
 include "nat/ord.ma".
index 211df69d0fa0d9941a9dcf14bebca51e1812ffda..752e89b9d02fec375326cd8d8df46b577daaef93 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-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).
index f391c85a9686e77900e11bee558cd07987e3fbf8..a222d36bab2df5b26df3782439656478c936caae 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/le_arith".
-
 include "nat/times.ma".
 include "nat/orders.ma".
 
index 39d9b2ecdfae7ecc55209fd8e979581fd28dbbc9..4c326ef25dcc19fe187ab98ef8e1cf04e1d584c6 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/log".
-
 include "datatypes/constructors.ma".
 include "nat/minimization.ma".
 include "nat/relevant_equations.ma".
index b4c31c526ca8bb321902661bc89040274349b99a..683ec262773cbe38541ba1499b6cf1eeb3775440 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/lt_arith".
-
 include "nat/div_and_mod.ma".
 
 (* plus *)
index 080f9a45fb883fc573d8945af970b0216c4d726c..0d3bac82c6572b33eca87f3c2dfdf6626280a9c5 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/map_iter_p.ma".
-
 include "nat/permutation.ma".
 include "nat/count.ma".
 
index 22d5030ddb37a12d032f66b489cd87aa7bc01780..d2cde9b67c56d1b961cfc8832fadbc0e67eaf43a 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/minimization".
-
 include "nat/minus.ma".
 
 let rec max i f \def
index 339e2262c72de402a1d29187e8a41907658038b7..a0133e93db58f65df22e64ca4e94944a26fda79e 100644 (file)
@@ -13,8 +13,6 @@
 (**************************************************************************)
 
 
-set "baseuri" "cic:/matita/nat/minus".
-
 include "nat/le_arith.ma".
 include "nat/compare.ma".
 
index daac5a23d3a4c658cc67e4ddd2af29bb8caac21b..85f598d129a434f7cad878dd9c8a2fc4fdc56077 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/nat".
-
 include "higher_order_defs/functions.ma".
 
 theorem esempio: \forall A,B,C:Prop.(A \to B \to C) \to (A \to B)
index bad55bc49c680d13dc32ed93db1fe515fb505e64..f200e62d6d8ff12c137df4f2cde17abdef8dc84c 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/neper".
-
 include "nat/iteration2.ma".
 include "nat/div_and_mod_diseq.ma".
 include "nat/binomial.ma".
index f675e80ba45717620d95a25c5081ca93bcd956c7..7b7c70bfe5cabfca704dce146034cb3ff1abad88 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/nth_prime".
-
 include "nat/primes.ma".
 include "nat/lt_arith.ma".
 
index 335550d0d6366f02d172c1f3aa6171d3ef6d171a..ab5f8a52aa87f5504d2b3950c3989653fd167aa0 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/ord".
-
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
 include "nat/nth_prime.ma".
index 799f8bf7c47b74c65575431e78d2f0b8f9662b9e..6336a5e9bf12bec1e9ddca458d5d98b36d1e548a 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/orders".
-
 include "nat/nat.ma".
 include "higher_order_defs/ordering.ma".
 
index 5d6e5cf1e953ca73cbe7d20f9347c4175a19c009..884c18ddc17c0f2a3dafe344c38dabb24160ec38 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/permutation".
-
 include "nat/compare.ma".
 include "nat/sigma_and_pi.ma".
 
index 9e820cd79bd2d5469f961a5cec32daaaae7e3147..93f127372410610e5147fe02c5bf3fa59a08b2c7 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/pi_p".
-
 include "nat/primes.ma".
 (* include "nat/ord.ma". *)
 include "nat/generic_iter_p.ma".
index e8b5f6d29e258cee77866c26a470f6cc4119bef5..09bd4e38decbdd477af3aae9745e6ef88a09f165 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/plus".
-
 include "nat/nat.ma".
 
 let rec plus n m \def 
index 0186d4324e3890666660282de63d5dc619a83520..dcf7abeea1372e0635817fb3a75554bd77b4bb0a 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/primes".
-
 include "nat/div_and_mod.ma".
 include "nat/minimization.ma".
 include "nat/sigma_and_pi.ma".
index 6e641708021d79d36c81b67283f889949e1fe43c..a2ef6e40cdc6ffaba378c058d3a030a6fa9bea9d 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/relevant_equations".
-
 include "nat/times.ma".
 include "nat/minus.ma".
 include "nat/gcd.ma". 
index 84301b49adf80d9aeab35c83b405bf8b50dc71f7..10727ed3ee492295f1e2414dc49bb2c548624532 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/sigma_and_pi".
-
 include "nat/factorial.ma".
 include "nat/exp.ma".
 include "nat/lt_arith.ma".
index f738e1cf28e0327a612c92e195017533cd840449..d523d634dc5ff3fb503fa34f1ca39eaf432fe040 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/sqrt/".
-
 include "nat/times.ma".
 include "nat/compare.ma".
 include "nat/log.ma".
index ec0f861998c2314536888bae8882de035fb21682..57dc60c6f2a071b5e25400161da998fa88f12763 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/times".
-
 include "nat/plus.ma".
 
 let rec times n m \def 
index 9933490a2dda03f20da09be3124dee5919ec3d8e..ecbfce554460d6433a14d3f3516823d4dfc8a8b9 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/totient".
-
 include "nat/chinese_reminder.ma".
 include "nat/iteration2.ma".
 
index c6b78ec90864ebea03557c675d267e8e2d6a3607..20c326d7d2ca00a91c7c2f3698523e8116e9eb5e 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/totient1".
-
 include "nat/totient.ma".
 include "nat/iteration2.ma".
 include "nat/gcd_properties1.ma".