--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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)
+ ].
(* *)
(**************************************************************************)
-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 *)
| 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.
| 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.
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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
-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
projects / helm.git / commitdiff