From: Claudio Sacerdoti Coen Date: Tue, 3 Jun 2008 21:58:35 +0000 (+0000) Subject: More work on rational numbers with unique representations. X-Git-Tag: make_still_working~5088 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c4cdbc2e7d115351a18adc6611c864b82fee61f;p=helm.git More work on rational numbers with unique representations. --- diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma new file mode 100644 index 000000000..6725f5c99 --- /dev/null +++ b/helm/software/matita/library/Q/inv.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "Q/q.ma". + +let rec finv f \def + match f with + [ (pp n) \Rightarrow (nn n) + | (nn n) \Rightarrow (pp n) + | (cons x g) \Rightarrow (cons (Zopp x) (finv g))]. + +definition rinv : ratio \to ratio \def +\lambda r:ratio. + match r with + [one \Rightarrow one + | (frac f) \Rightarrow frac (finv f)]. + +definition Qinv : Q → Q ≝ + λp. + match p with + [ OQ ⇒ OQ (* arbitrary value *) + | Qpos r ⇒ Qpos (rinv r) + | Qneg r ⇒ Qneg (rinv r) + ]. diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma index 072532d7b..af70c3b73 100644 --- a/helm/software/matita/library/Q/q.ma +++ b/helm/software/matita/library/Q/q.ma @@ -12,10 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Q/q". - include "Z/compare.ma". include "Z/plus.ma". +include "nat/factorization.ma". (* a fraction is a list of Z-coefficients for primes, in natural order. The last coefficient must eventually be different from 0 *) @@ -25,6 +24,36 @@ inductive fraction : Set \def | nn: nat \to fraction | cons : Z \to fraction \to fraction. +let rec fraction_of_nat_fact n ≝ + match n with + [ nf_last m ⇒ pp m + | nf_cons m l ⇒ cons (Z_of_nat (S m)) (fraction_of_nat_fact l) + ]. + +(* a fraction is integral if every coefficient is not negative *) +let rec nat_fact_of_integral_fraction n ≝ + match n with + [ pp n ⇒ nf_last n + | nn _ ⇒ nf_last O (* dummy value *) + | cons z l ⇒ + match z with + [ OZ ⇒ nf_cons O (nat_fact_of_integral_fraction l) + | pos n ⇒ nf_cons n (nat_fact_of_integral_fraction l) + | neg n ⇒ nf_last O (* dummy value *) + ] + ]. + +theorem nat_fact_of_integral_fraction_fraction_of_nat_fact: + ∀n. nat_fact_of_integral_fraction (fraction_of_nat_fact n) = n. + intro; + elim n; + [ reflexivity; + | simplify; + rewrite > H; + reflexivity + ] +qed. + inductive ratio : Set \def one : ratio | frac : fraction \to ratio. @@ -35,6 +64,93 @@ inductive Q : Set \def | Qpos : ratio \to Q | Qneg : ratio \to Q. +definition Q_of_nat ≝ + λn. + match factorize n with + [ nfa_zero ⇒ OQ + | nfa_one ⇒ Qpos one + | nfa_proper l ⇒ Qpos (frac (fraction_of_nat_fact l)) + ]. + +let rec enumerator_integral_fraction l ≝ + match l with + [ pp n ⇒ Some ? l + | nn _ ⇒ None ? + | cons z r ⇒ + match enumerator_integral_fraction r with + [ None ⇒ + match z with + [ pos n ⇒ Some ? (pp n) + | _ ⇒ None ? + ] + | Some r' ⇒ + Some ? + match z with + [ neg _ ⇒ cons OZ r' + | _ ⇒ cons z r' + ] + ] + ]. + +let rec denominator_integral_fraction l ≝ + match l with + [ pp _ ⇒ None ? + | nn n ⇒ Some ? (pp n) + | cons z r ⇒ + match denominator_integral_fraction r with + [ None ⇒ + match z with + [ neg n ⇒ Some ? (pp n) + | _ ⇒ None ? + ] + | Some r' ⇒ + Some ? + match z with + [ pos _ ⇒ cons OZ r' + | neg m ⇒ cons (pos m) r' + | OZ ⇒ cons OZ r' + ] + ] + ]. + +definition enumerator_of_fraction ≝ + λq. + match q with + [ one ⇒ S O + | frac f ⇒ + match enumerator_integral_fraction f with + [ None ⇒ S O + | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O + ] + ]. + +definition denominator_of_fraction ≝ + λq. + match q with + [ one ⇒ S O + | frac f ⇒ + match denominator_integral_fraction f with + [ None ⇒ S O + | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O + ] + ]. + +definition enumerator ≝ + λq. + match q with + [ OQ ⇒ OZ + | Qpos r ⇒ pos (pred (enumerator_of_fraction r)) + | Qneg r ⇒ neg(pred (enumerator_of_fraction r)) + ]. + +definition denominator ≝ + λq. + match q with + [ OQ ⇒ S O + | Qpos r ⇒ denominator_of_fraction r + | Qneg r ⇒ denominator_of_fraction r + ]. + (* double elimination principles *) theorem fraction_elim2: \forall R:fraction \to fraction \to Prop. @@ -207,135 +323,3 @@ intros.apply (fraction_elim2 simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption. intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption. qed. - -let rec finv f \def - match f with - [ (pp n) \Rightarrow (nn n) - | (nn n) \Rightarrow (pp n) - | (cons x g) \Rightarrow (cons (Zopp x) (finv g))]. - -definition Z_to_ratio :Z \to ratio \def -\lambda x:Z. match x with -[ OZ \Rightarrow one -| (pos n) \Rightarrow frac (pp n) -| (neg n) \Rightarrow frac (nn n)]. - -let rec ftimes f g \def - match f with - [ (pp n) \Rightarrow - match g with - [(pp m) \Rightarrow Z_to_ratio (pos n + pos m) - | (nn m) \Rightarrow Z_to_ratio (pos n + neg m) - | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)] - | (nn n) \Rightarrow - match g with - [(pp m) \Rightarrow Z_to_ratio (neg n + pos m) - | (nn m) \Rightarrow Z_to_ratio (neg n + neg m) - | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)] - | (cons x f1) \Rightarrow - match g with - [ (pp m) \Rightarrow frac (cons (x + pos m) f1) - | (nn m) \Rightarrow frac (cons (x + neg m) f1) - | (cons y g1) \Rightarrow - match ftimes f1 g1 with - [ one \Rightarrow Z_to_ratio (x + y) - | (frac h) \Rightarrow frac (cons (x + y) h)]]]. - -theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes. -unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)). - intros.elim g. - change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)). - apply eq_f.apply sym_Zplus. - change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)). - apply eq_f.apply sym_Zplus. - change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)). - rewrite < sym_Zplus.reflexivity. - intros.elim g. - change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)). - apply eq_f.apply sym_Zplus. - change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)). - apply eq_f.apply sym_Zplus. - change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)). - rewrite < sym_Zplus.reflexivity. - intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)). - rewrite < sym_Zplus.reflexivity. - intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)). - rewrite < sym_Zplus.reflexivity. - intros. - (*CSC: simplify does something nasty here because of a redex in Zplus *) - change with - (match ftimes f g with - [ one \Rightarrow Z_to_ratio (x1 + y1) - | (frac h) \Rightarrow frac (cons (x1 + y1) h)] = - match ftimes g f with - [ one \Rightarrow Z_to_ratio (y1 + x1) - | (frac h) \Rightarrow frac (cons (y1 + x1) h)]). - rewrite < H.rewrite < sym_Zplus.reflexivity. -qed. - -theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one. -intro.elim f. - change with (Z_to_ratio (pos n + - (pos n)) = one). - rewrite > Zplus_Zopp.reflexivity. - change with (Z_to_ratio (neg n + - (neg n)) = one). - rewrite > Zplus_Zopp.reflexivity. - (*CSC: simplify does something nasty here because of a redex in Zplus *) -(* again: we would need something to help finding the right change *) - change with - (match ftimes f1 (finv f1) with - [ one \Rightarrow Z_to_ratio (z + - z) - | (frac h) \Rightarrow frac (cons (z + - z) h)] = one). - rewrite > H.rewrite > Zplus_Zopp.reflexivity. -qed. - -definition rtimes : ratio \to ratio \to ratio \def -\lambda r,s:ratio. - match r with - [one \Rightarrow s - | (frac f) \Rightarrow - match s with - [one \Rightarrow frac f - | (frac g) \Rightarrow ftimes f g]]. - -theorem symmetric_rtimes : symmetric ratio rtimes. -change with (\forall r,s:ratio. rtimes r s = rtimes s r). -intros. -elim r. elim s. -reflexivity. -reflexivity. -elim s. -reflexivity. -simplify.apply symmetric2_ftimes. -qed. - -definition rinv : ratio \to ratio \def -\lambda r:ratio. - match r with - [one \Rightarrow one - | (frac f) \Rightarrow frac (finv f)]. - -theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one. -intro.elim r. -reflexivity. -simplify.apply ftimes_finv. -qed. - -definition Qtimes : Q \to Q \to Q \def -\lambda p,q. - match p with - [OQ \Rightarrow OQ - |Qpos p1 \Rightarrow - match q with - [OQ \Rightarrow OQ - |Qpos q1 \Rightarrow Qpos (rtimes p1 q1) - |Qneg q1 \Rightarrow Qneg (rtimes p1 q1) - ] - |Qneg p1 \Rightarrow - match q with - [OQ \Rightarrow OQ - |Qpos q1 \Rightarrow Qneg (rtimes p1 q1) - |Qneg q1 \Rightarrow Qpos (rtimes p1 q1) - ] - ] -. - \ No newline at end of file diff --git a/helm/software/matita/library/Q/times.ma b/helm/software/matita/library/Q/times.ma new file mode 100644 index 000000000..2f625ba9b --- /dev/null +++ b/helm/software/matita/library/Q/times.ma @@ -0,0 +1,164 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "Q/inv.ma". + +definition Z_to_ratio: Z \to ratio \def +\lambda x:Z. match x with +[ OZ \Rightarrow one +| (pos n) \Rightarrow frac (pp n) +| (neg n) \Rightarrow frac (nn n)]. + +let rec ftimes f g \def + match f with + [ (pp n) \Rightarrow + match g with + [(pp m) \Rightarrow Z_to_ratio (pos n + pos m) + | (nn m) \Rightarrow Z_to_ratio (pos n + neg m) + | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)] + | (nn n) \Rightarrow + match g with + [(pp m) \Rightarrow Z_to_ratio (neg n + pos m) + | (nn m) \Rightarrow Z_to_ratio (neg n + neg m) + | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)] + | (cons x f1) \Rightarrow + match g with + [ (pp m) \Rightarrow frac (cons (x + pos m) f1) + | (nn m) \Rightarrow frac (cons (x + neg m) f1) + | (cons y g1) \Rightarrow + match ftimes f1 g1 with + [ one \Rightarrow Z_to_ratio (x + y) + | (frac h) \Rightarrow frac (cons (x + y) h)]]]. + +theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes. +unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)). + intros.elim g. + change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)). + apply eq_f.apply sym_Zplus. + change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)). + apply eq_f.apply sym_Zplus. + change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)). + rewrite < sym_Zplus.reflexivity. + intros.elim g. + change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)). + apply eq_f.apply sym_Zplus. + change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)). + apply eq_f.apply sym_Zplus. + change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)). + rewrite < sym_Zplus.reflexivity. + intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)). + rewrite < sym_Zplus.reflexivity. + intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)). + rewrite < sym_Zplus.reflexivity. + intros. + (*CSC: simplify does something nasty here because of a redex in Zplus *) + change with + (match ftimes f g with + [ one \Rightarrow Z_to_ratio (x1 + y1) + | (frac h) \Rightarrow frac (cons (x1 + y1) h)] = + match ftimes g f with + [ one \Rightarrow Z_to_ratio (y1 + x1) + | (frac h) \Rightarrow frac (cons (y1 + x1) h)]). + rewrite < H.rewrite < sym_Zplus.reflexivity. +qed. + +theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one. +intro.elim f. + change with (Z_to_ratio (pos n + - (pos n)) = one). + rewrite > Zplus_Zopp.reflexivity. + change with (Z_to_ratio (neg n + - (neg n)) = one). + rewrite > Zplus_Zopp.reflexivity. + (*CSC: simplify does something nasty here because of a redex in Zplus *) +(* again: we would need something to help finding the right change *) + change with + (match ftimes f1 (finv f1) with + [ one \Rightarrow Z_to_ratio (z + - z) + | (frac h) \Rightarrow frac (cons (z + - z) h)] = one). + rewrite > H.rewrite > Zplus_Zopp.reflexivity. +qed. + +definition rtimes : ratio \to ratio \to ratio \def +\lambda r,s:ratio. + match r with + [one \Rightarrow s + | (frac f) \Rightarrow + match s with + [one \Rightarrow frac f + | (frac g) \Rightarrow ftimes f g]]. + +theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one. +intro.elim r. +reflexivity. +simplify.apply ftimes_finv. +qed. + +theorem symmetric_rtimes : symmetric ratio rtimes. +change with (\forall r,s:ratio. rtimes r s = rtimes s r). +intros. +elim r. elim s. +reflexivity. +reflexivity. +elim s. +reflexivity. +simplify.apply symmetric2_ftimes. +qed. + +variant sym_rtimes : ∀x,y:ratio. rtimes x y = rtimes y x ≝ symmetric_rtimes. + +definition Qtimes : Q \to Q \to Q \def +\lambda p,q. + match p with + [OQ \Rightarrow OQ + |Qpos p1 \Rightarrow + match q with + [OQ \Rightarrow OQ + |Qpos q1 \Rightarrow Qpos (rtimes p1 q1) + |Qneg q1 \Rightarrow Qneg (rtimes p1 q1) + ] + |Qneg p1 \Rightarrow + match q with + [OQ \Rightarrow OQ + |Qpos q1 \Rightarrow Qneg (rtimes p1 q1) + |Qneg q1 \Rightarrow Qpos (rtimes p1 q1) + ] + ]. + +interpretation "rational times" 'times x y = (cic:/matita/Q/times/Qtimes.con x y). + +theorem Qtimes_q_OQ: ∀q. q * OQ = OQ. + intro; + elim q; + reflexivity. +qed. + +theorem symmetric_Qtimes: symmetric ? Qtimes. + intros 2; + elim x; + [ rewrite > Qtimes_q_OQ; reflexivity + |*:elim y; + simplify; + try rewrite > sym_rtimes; + reflexivity + ] +qed. + +theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one. + intro; + elim q; + [ elim H; reflexivity + |*:simplify; + rewrite > rtimes_rinv; + reflexivity + ] +qed. diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 76ed2b134..b274f1b91 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,81 +1,83 @@ -Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma +list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma +list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma +list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma Z/moebius.ma Z/sigma_p.ma nat/factorization.ma -Z/times.ma Z/plus.ma nat/lt_arith.ma -Z/orders.ma Z/z.ma logic/connectives.ma nat/orders.ma -Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma Z/plus.ma Z/z.ma nat/minus.ma Z/compare.ma Z/orders.ma nat/compare.ma -Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma Z/z.ma datatypes/bool.ma nat/nat.ma -datatypes/constructors.ma logic/equality.ma +Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma +Z/orders.ma Z/z.ma logic/connectives.ma nat/orders.ma +Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +Z/times.ma Z/plus.ma nat/lt_arith.ma +decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma +decidable_kit/fgraph.ma decidable_kit/fintype.ma +decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma +decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma +decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma +decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma +higher_order_defs/functions.ma logic/equality.ma +higher_order_defs/ordering.ma logic/equality.ma +higher_order_defs/relations.ma logic/connectives.ma +Q/q.ma Z/compare.ma Z/plus.ma nat/factorization.ma +Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma +Q/times.ma Q/inv.ma Q/q.ma +Q/inv.ma Q/q.ma datatypes/compare.ma +datatypes/constructors.ma logic/equality.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma -algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma +algebra/monoids.ma algebra/semigroups.ma algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma algebra/semigroups.ma higher_order_defs/functions.ma -algebra/monoids.ma algebra/semigroups.ma -demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma -demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma -demo/realisability.ma datatypes/constructors.ma logic/connectives.ma -list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma -list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma -list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma +algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma +logic/coimplication.ma logic/connectives.ma logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma logic/connectives.ma -logic/coimplication.ma logic/connectives.ma logic/connectives2.ma higher_order_defs/relations.ma -nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma -nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma -nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma +technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma +demo/realisability.ma datatypes/constructors.ma logic/connectives.ma +demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma +demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma +nat/plus.ma nat/nat.ma +nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma +nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma +nat/factorial2.ma nat/exp.ma nat/factorial.ma +nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma +nat/le_arith.ma nat/orders.ma nat/times.ma +nat/chebyshev_thm.ma nat/neper.ma nat/congruence.ma nat/primes.ma nat/relevant_equations.ma +nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma +nat/div_and_mod_diseq.ma nat/lt_arith.ma +nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma +nat/gcd_properties1.ma nat/gcd.ma +nat/binomial.ma nat/factorial2.ma nat/iteration2.ma nat/minus.ma nat/compare.ma nat/le_arith.ma -nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma -nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma -nat/factorial.ma nat/le_arith.ma -nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma -nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma +nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma +nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma nat/minimization.ma nat/minus.ma -nat/gcd.ma nat/lt_arith.ma nat/primes.ma +nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma -nat/le_arith.ma nat/orders.ma nat/times.ma -nat/times.ma nat/plus.ma -nat/gcd_properties1.ma nat/gcd.ma -nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma -nat/lt_arith.ma nat/div_and_mod.ma -nat/factorization.ma nat/ord.ma nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma -nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma -nat/factorial2.ma nat/exp.ma nat/factorial.ma -nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma +nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma nat/nat.ma higher_order_defs/functions.ma -nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma -nat/map_iter_p.ma nat/count.ma nat/permutation.ma -nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma -nat/plus.ma nat/nat.ma +nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma +nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma +nat/gcd.ma nat/lt_arith.ma nat/primes.ma +nat/o.ma nat/binomial.ma nat/sqrt.ma +nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma -nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma -nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma +nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma +nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma +nat/factorial.ma nat/le_arith.ma +nat/lt_arith.ma nat/div_and_mod.ma +nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma +nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma +nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma +nat/factorization.ma nat/ord.ma +nat/map_iter_p.ma nat/count.ma nat/permutation.ma +nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma -nat/chebyshev_thm.ma nat/neper.ma -nat/div_and_mod_diseq.ma nat/lt_arith.ma -nat/binomial.ma nat/factorial2.ma nat/iteration2.ma -nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma -nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma -nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma -nat/o.ma nat/binomial.ma nat/sqrt.ma -nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma -Q/q.ma Z/compare.ma Z/plus.ma -Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma -decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma -decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma -decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma -decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma -decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma -decidable_kit/fgraph.ma decidable_kit/fintype.ma -higher_order_defs/relations.ma logic/connectives.ma -higher_order_defs/functions.ma logic/equality.ma -higher_order_defs/ordering.ma logic/equality.ma +nat/times.ma nat/plus.ma