From c445ba5534cccde19016c92660ab52777af221c0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 18 Feb 2008 08:56:40 +0000 Subject: [PATCH] Complete proof of Bertrand for n >= 256. Removed the baseuri form all files in nat. --- helm/software/matita/library/nat/bertrand.ma | 257 +++++++++++++++++- helm/software/matita/library/nat/binomial.ma | 2 - .../matita/library/nat/chebyshev_teta.ma | 2 - .../matita/library/nat/chebyshev_thm.ma | 2 - .../matita/library/nat/chinese_reminder.ma | 2 - helm/software/matita/library/nat/compare.ma | 2 - .../software/matita/library/nat/congruence.ma | 2 - helm/software/matita/library/nat/count.ma | 2 - .../matita/library/nat/div_and_mod.ma | 3 - .../matita/library/nat/div_and_mod_diseq.ma | 2 - .../matita/library/nat/euler_theorem.ma | 2 - helm/software/matita/library/nat/exp.ma | 2 - helm/software/matita/library/nat/factorial.ma | 2 - .../software/matita/library/nat/factorial2.ma | 2 - .../matita/library/nat/factorization.ma | 2 - .../library/nat/fermat_little_theorem.ma | 2 - helm/software/matita/library/nat/gcd.ma | 2 - .../matita/library/nat/generic_iter_p.ma | 2 - .../software/matita/library/nat/iteration2.ma | 3 - helm/software/matita/library/nat/le_arith.ma | 2 - helm/software/matita/library/nat/log.ma | 2 - helm/software/matita/library/nat/lt_arith.ma | 2 - .../software/matita/library/nat/map_iter_p.ma | 2 - .../matita/library/nat/minimization.ma | 2 - helm/software/matita/library/nat/minus.ma | 2 - helm/software/matita/library/nat/nat.ma | 2 - helm/software/matita/library/nat/neper.ma | 2 - helm/software/matita/library/nat/nth_prime.ma | 2 - helm/software/matita/library/nat/ord.ma | 2 - helm/software/matita/library/nat/orders.ma | 2 - .../matita/library/nat/permutation.ma | 2 - helm/software/matita/library/nat/pi_p.ma | 2 - helm/software/matita/library/nat/plus.ma | 2 - helm/software/matita/library/nat/primes.ma | 2 - .../matita/library/nat/relevant_equations.ma | 2 - .../matita/library/nat/sigma_and_pi.ma | 2 - helm/software/matita/library/nat/sqrt.ma | 2 - helm/software/matita/library/nat/times.ma | 2 - helm/software/matita/library/nat/totient.ma | 2 - helm/software/matita/library/nat/totient1.ma | 2 - 40 files changed, 253 insertions(+), 84 deletions(-) diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index f014b0ecc..20302e876 100644 --- a/helm/software/matita/library/nat/bertrand.ma +++ b/helm/software/matita/library/nat/bertrand.ma @@ -15,10 +15,64 @@ 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. +*) diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma index e7d58039a..83ef0acbb 100644 --- a/helm/software/matita/library/nat/binomial.ma +++ b/helm/software/matita/library/nat/binomial.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/binomial". - include "nat/iteration2.ma". include "nat/factorial2.ma". diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma index 4c839892a..1765b3807 100644 --- a/helm/software/matita/library/nat/chebyshev_teta.ma +++ b/helm/software/matita/library/nat/chebyshev_teta.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/chebyshev_teta". - include "nat/binomial.ma". include "nat/pi_p.ma". diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma index 248c9e3c6..e90b22d9d 100644 --- a/helm/software/matita/library/nat/chebyshev_thm.ma +++ b/helm/software/matita/library/nat/chebyshev_thm.ma @@ -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 diff --git a/helm/software/matita/library/nat/chinese_reminder.ma b/helm/software/matita/library/nat/chinese_reminder.ma index 766b85f71..2bf3bc59e 100644 --- a/helm/software/matita/library/nat/chinese_reminder.ma +++ b/helm/software/matita/library/nat/chinese_reminder.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/chinese_reminder". - include "nat/exp.ma". include "nat/gcd.ma". include "nat/permutation.ma". diff --git a/helm/software/matita/library/nat/compare.ma b/helm/software/matita/library/nat/compare.ma index b002d78cc..dd9589e7b 100644 --- a/helm/software/matita/library/nat/compare.ma +++ b/helm/software/matita/library/nat/compare.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/compare". - include "datatypes/bool.ma". include "datatypes/compare.ma". include "nat/orders.ma". diff --git a/helm/software/matita/library/nat/congruence.ma b/helm/software/matita/library/nat/congruence.ma index f418c1b85..753745d45 100644 --- a/helm/software/matita/library/nat/congruence.ma +++ b/helm/software/matita/library/nat/congruence.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/congruence". - include "nat/relevant_equations.ma". include "nat/primes.ma". diff --git a/helm/software/matita/library/nat/count.ma b/helm/software/matita/library/nat/count.ma index 2abcf25c3..6b5dbbe66 100644 --- a/helm/software/matita/library/nat/count.ma +++ b/helm/software/matita/library/nat/count.ma @@ -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". diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma index 523f74314..538515a8c 100644 --- a/helm/software/matita/library/nat/div_and_mod.ma +++ b/helm/software/matita/library/nat/div_and_mod.ma @@ -12,12 +12,9 @@ (* *) (**************************************************************************) -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 diff --git a/helm/software/matita/library/nat/div_and_mod_diseq.ma b/helm/software/matita/library/nat/div_and_mod_diseq.ma index 299897a38..464998223 100644 --- a/helm/software/matita/library/nat/div_and_mod_diseq.ma +++ b/helm/software/matita/library/nat/div_and_mod_diseq.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/div_and_mod_diseq". - include "nat/lt_arith.ma". (* the proof that diff --git a/helm/software/matita/library/nat/euler_theorem.ma b/helm/software/matita/library/nat/euler_theorem.ma index 1e5988b35..9396d444e 100644 --- a/helm/software/matita/library/nat/euler_theorem.ma +++ b/helm/software/matita/library/nat/euler_theorem.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/euler_theorem". - include "nat/map_iter_p.ma". include "nat/totient.ma". diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma index 52793cb5a..c9f2c6984 100644 --- a/helm/software/matita/library/nat/exp.ma +++ b/helm/software/matita/library/nat/exp.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/exp". - include "nat/div_and_mod.ma". include "nat/lt_arith.ma". diff --git a/helm/software/matita/library/nat/factorial.ma b/helm/software/matita/library/nat/factorial.ma index 14217bbcb..58220cb0c 100644 --- a/helm/software/matita/library/nat/factorial.ma +++ b/helm/software/matita/library/nat/factorial.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/factorial". - include "nat/le_arith.ma". let rec fact n \def diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma index 6215d6657..bcd228d08 100644 --- a/helm/software/matita/library/nat/factorial2.ma +++ b/helm/software/matita/library/nat/factorial2.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/factorial2". - include "nat/exp.ma". include "nat/factorial.ma". diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index 8c50d1d7d..1ca684aed 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/factorization". - include "nat/ord.ma". (* the following factorization algorithm looks for the largest prime diff --git a/helm/software/matita/library/nat/fermat_little_theorem.ma b/helm/software/matita/library/nat/fermat_little_theorem.ma index f7953346a..1dc6669cb 100644 --- a/helm/software/matita/library/nat/fermat_little_theorem.ma +++ b/helm/software/matita/library/nat/fermat_little_theorem.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/fermat_little_theorem". - include "nat/exp.ma". include "nat/gcd.ma". include "nat/permutation.ma". diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma index 0baa86e3c..3db29f622 100644 --- a/helm/software/matita/library/nat/gcd.ma +++ b/helm/software/matita/library/nat/gcd.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/gcd". - include "nat/primes.ma". include "nat/lt_arith.ma". diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma index f89c32f87..5f15bddc9 100644 --- a/helm/software/matita/library/nat/generic_iter_p.ma +++ b/helm/software/matita/library/nat/generic_iter_p.ma @@ -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". diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma index 211df69d0..752e89b9d 100644 --- 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). diff --git a/helm/software/matita/library/nat/le_arith.ma b/helm/software/matita/library/nat/le_arith.ma index f391c85a9..a222d36ba 100644 --- a/helm/software/matita/library/nat/le_arith.ma +++ b/helm/software/matita/library/nat/le_arith.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/le_arith". - include "nat/times.ma". include "nat/orders.ma". diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma index 39d9b2ecd..4c326ef25 100644 --- a/helm/software/matita/library/nat/log.ma +++ b/helm/software/matita/library/nat/log.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/log". - include "datatypes/constructors.ma". include "nat/minimization.ma". include "nat/relevant_equations.ma". diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma index b4c31c526..683ec2627 100644 --- a/helm/software/matita/library/nat/lt_arith.ma +++ b/helm/software/matita/library/nat/lt_arith.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/lt_arith". - include "nat/div_and_mod.ma". (* plus *) diff --git a/helm/software/matita/library/nat/map_iter_p.ma b/helm/software/matita/library/nat/map_iter_p.ma index 080f9a45f..0d3bac82c 100644 --- a/helm/software/matita/library/nat/map_iter_p.ma +++ b/helm/software/matita/library/nat/map_iter_p.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/map_iter_p.ma". - include "nat/permutation.ma". include "nat/count.ma". diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma index 22d5030dd..d2cde9b67 100644 --- a/helm/software/matita/library/nat/minimization.ma +++ b/helm/software/matita/library/nat/minimization.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/minimization". - include "nat/minus.ma". let rec max i f \def diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma index 339e2262c..a0133e93d 100644 --- a/helm/software/matita/library/nat/minus.ma +++ b/helm/software/matita/library/nat/minus.ma @@ -13,8 +13,6 @@ (**************************************************************************) -set "baseuri" "cic:/matita/nat/minus". - include "nat/le_arith.ma". include "nat/compare.ma". diff --git a/helm/software/matita/library/nat/nat.ma b/helm/software/matita/library/nat/nat.ma index daac5a23d..85f598d12 100644 --- a/helm/software/matita/library/nat/nat.ma +++ b/helm/software/matita/library/nat/nat.ma @@ -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) diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index bad55bc49..f200e62d6 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -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". diff --git a/helm/software/matita/library/nat/nth_prime.ma b/helm/software/matita/library/nat/nth_prime.ma index f675e80ba..7b7c70bfe 100644 --- a/helm/software/matita/library/nat/nth_prime.ma +++ b/helm/software/matita/library/nat/nth_prime.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/nth_prime". - include "nat/primes.ma". include "nat/lt_arith.ma". diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index 335550d0d..ab5f8a52a 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/matita/library/nat/ord.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/ord". - include "datatypes/constructors.ma". include "nat/exp.ma". include "nat/nth_prime.ma". diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma index 799f8bf7c..6336a5e9b 100644 --- a/helm/software/matita/library/nat/orders.ma +++ b/helm/software/matita/library/nat/orders.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/orders". - include "nat/nat.ma". include "higher_order_defs/ordering.ma". diff --git a/helm/software/matita/library/nat/permutation.ma b/helm/software/matita/library/nat/permutation.ma index 5d6e5cf1e..884c18ddc 100644 --- a/helm/software/matita/library/nat/permutation.ma +++ b/helm/software/matita/library/nat/permutation.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/permutation". - include "nat/compare.ma". include "nat/sigma_and_pi.ma". diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma index 9e820cd79..93f127372 100644 --- a/helm/software/matita/library/nat/pi_p.ma +++ b/helm/software/matita/library/nat/pi_p.ma @@ -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". diff --git a/helm/software/matita/library/nat/plus.ma b/helm/software/matita/library/nat/plus.ma index e8b5f6d29..09bd4e38d 100644 --- a/helm/software/matita/library/nat/plus.ma +++ b/helm/software/matita/library/nat/plus.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/plus". - include "nat/nat.ma". let rec plus n m \def diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma index 0186d4324..dcf7abeea 100644 --- a/helm/software/matita/library/nat/primes.ma +++ b/helm/software/matita/library/nat/primes.ma @@ -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". diff --git a/helm/software/matita/library/nat/relevant_equations.ma b/helm/software/matita/library/nat/relevant_equations.ma index 6e6417080..a2ef6e40c 100644 --- a/helm/software/matita/library/nat/relevant_equations.ma +++ b/helm/software/matita/library/nat/relevant_equations.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/relevant_equations". - include "nat/times.ma". include "nat/minus.ma". include "nat/gcd.ma". diff --git a/helm/software/matita/library/nat/sigma_and_pi.ma b/helm/software/matita/library/nat/sigma_and_pi.ma index 84301b49a..10727ed3e 100644 --- a/helm/software/matita/library/nat/sigma_and_pi.ma +++ b/helm/software/matita/library/nat/sigma_and_pi.ma @@ -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". diff --git a/helm/software/matita/library/nat/sqrt.ma b/helm/software/matita/library/nat/sqrt.ma index f738e1cf2..d523d634d 100644 --- a/helm/software/matita/library/nat/sqrt.ma +++ b/helm/software/matita/library/nat/sqrt.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/sqrt/". - include "nat/times.ma". include "nat/compare.ma". include "nat/log.ma". diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma index ec0f86199..57dc60c6f 100644 --- a/helm/software/matita/library/nat/times.ma +++ b/helm/software/matita/library/nat/times.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/times". - include "nat/plus.ma". let rec times n m \def diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma index 9933490a2..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". diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma index c6b78ec90..20c326d7d 100644 --- a/helm/software/matita/library/nat/totient1.ma +++ b/helm/software/matita/library/nat/totient1.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/totient1". - include "nat/totient.ma". include "nat/iteration2.ma". include "nat/gcd_properties1.ma". -- 2.39.2