diff options
Diffstat (limited to 'theories/Numbers/NatInt')
-rw-r--r-- | theories/Numbers/NatInt/NZAdd.v | 8 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZAddOrder.v | 23 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 4 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 9 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZDomain.v | 2 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZMul.v | 22 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZMulOrder.v | 6 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 24 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZPow.v | 358 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZProperties.v | 4 |
10 files changed, 425 insertions, 35 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index bceea42b7..7d7cc4ac5 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -10,8 +10,7 @@ Require Import NZAxioms NZBase. -Module Type NZAddPropSig - (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). +Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). Hint Rewrite pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. @@ -76,8 +75,7 @@ Qed. Theorem add_shuffle2 : forall n m p q, (n + m) + (p + q) == (n + q) + (m + p). Proof. -intros n m p q. -rewrite 2 add_assoc, add_shuffle0, add_cancel_r. apply add_shuffle0. +intros n m p q. rewrite (add_comm p). apply add_shuffle1. Qed. Theorem sub_1_r : forall n, n - 1 == P n. @@ -85,4 +83,4 @@ Proof. intro n; now nzsimpl. Qed. -End NZAddPropSig. +End NZAddProp. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index b715b4b00..3aa6f41d3 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -10,8 +10,8 @@ Require Import NZAxioms NZBase NZMul NZOrder. -Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig'). -Include NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ. +Module Type NZAddOrderProp (Import NZ : NZOrdAxiomsSig'). +Include NZBaseProp NZ <+ NZMulProp NZ <+ NZOrderProp NZ. Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m. Proof. @@ -147,5 +147,22 @@ Proof. intros n m H; apply add_le_cases; now nzsimpl. Qed. -End NZAddOrderPropSig. +(** Substraction *) + +(** We can prove the existence of a subtraction of any number by + a smaller one *) + +Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p. +Proof. + intros n m H. apply le_ind with (4:=H). solve_predicate_wd. + exists 0; nzsimpl; split; order. + clear m H. intros m H (p & EQ & LE). exists (S p). + split. nzsimpl. now apply succ_wd. now apply le_le_succ_r. +Qed. + +(** For the moment, it doesn't seem possible to relate + this existing subtraction with [sub]. +*) + +End NZAddOrderProp. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index d2437e354..a86fec3fd 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -10,7 +10,7 @@ Require Import NZAxioms. -Module Type NZBasePropSig (Import NZ : NZDomainSig'). +Module Type NZBaseProp (Import NZ : NZDomainSig'). Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *) @@ -83,5 +83,5 @@ Tactic Notation "nzinduct" ident(n) := Tactic Notation "nzinduct" ident(n) constr(u) := induction_maker n ltac:(apply central_induction with (z := u)). -End NZBasePropSig. +End NZBaseProp. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 75f0206f8..3b9720f32 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -45,11 +45,10 @@ Module Type NZDiv (NZ:NZOrdAxiomsSig) Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ. -Module NZDivPropFunct +Module NZDivProp (Import NZ : NZOrdAxiomsSig') - (Import NZP : NZMulOrderPropSig NZ) - (Import NZD : NZDiv' NZ) -. + (Import NZP : NZMulOrderProp NZ) + (Import NZD : NZDiv' NZ). (** Uniqueness theorems *) @@ -538,5 +537,5 @@ Proof. rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. Qed. -End NZDivPropFunct. +End NZDivProp. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index f07c55524..a26e93d76 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -305,7 +305,7 @@ End NZOfNat. Module NZOfNatOrd (Import NZ:NZOrdSig'). Include NZOfNat NZ. -Include NZOrderPropFunct NZ. +Include NZBaseProp NZ <+ NZOrderProp NZ. Local Open Scope ofnat. Theorem ofnat_S_gt_0 : diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index a87d6ac62..55ec3f30e 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -10,9 +10,8 @@ Require Import NZAxioms NZBase NZAdd. -Module Type NZMulPropSig - (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). -Include NZAddPropSig NZ NZBase. +Module Type NZMulProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). +Include NZAddProp NZ NZBase. Theorem mul_0_r : forall n, n * 0 == 0. Proof. @@ -65,4 +64,19 @@ Proof. intro n. now nzsimpl. Qed. -End NZMulPropSig. +Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m. +Proof. +intros n m p. now rewrite <- 2 mul_assoc, (mul_comm m). +Qed. + +Theorem mul_shuffle1 : forall n m p q, (n * m) * (p * q) == (n * p) * (m * q). +Proof. +intros n m p q. now rewrite 2 mul_assoc, (mul_shuffle0 n). +Qed. + +Theorem mul_shuffle2 : forall n m p q, (n * m) * (p * q) == (n * q) * (m * p). +Proof. +intros n m p q. rewrite (mul_comm p). apply mul_shuffle1. +Qed. + +End NZMulProp. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 414931ba8..530044ab0 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -11,8 +11,8 @@ Require Import NZAxioms. Require Import NZAddOrder. -Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig'). -Include NZAddOrderPropSig NZ. +Module Type NZMulOrderProp (Import NZ : NZOrdAxiomsSig'). +Include NZAddOrderProp NZ. Theorem mul_lt_pred : forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). @@ -302,4 +302,4 @@ rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l. apply add_pos_pos; now apply lt_0_1. Qed. -End NZMulOrderPropSig. +End NZMulOrderProp. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 8fdf8b47e..93201964e 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -10,8 +10,8 @@ Require Import NZAxioms NZBase Decidable OrdersTac. -Module Type NZOrderPropSig - (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ). +Module Type NZOrderProp + (Import NZ : NZOrdSig')(Import NZBase : NZBaseProp NZ). Instance le_wd : Proper (eq==>eq==>iff) le. Proof. @@ -357,6 +357,13 @@ intros z n H; apply lt_exists_pred_strong with (z := z) (n := n). assumption. apply le_refl. Qed. +Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n. +Proof. + intros z n H. + destruct (lt_exists_pred _ _ H) as (n' & EQ & LE). + rewrite EQ. now rewrite pred_succ. +Qed. + (** Stronger variant of induction with assumptions n >= 0 (n < 0) in the induction step *) @@ -557,7 +564,7 @@ apply right_induction with (S n); [assumption | | now apply <- le_succ_l]. intros; apply H2; try assumption. now apply -> le_succ_l. Qed. -(** Elimintation principle for <= *) +(** Elimination principle for <= *) Theorem le_ind : forall (n : t), A n -> @@ -628,15 +635,12 @@ Qed. End WF. -End NZOrderPropSig. - -Module NZOrderPropFunct (NZ : NZOrdSig) := - NZBasePropSig NZ <+ NZOrderPropSig NZ. +End NZOrderProp. (** If we have moreover a [compare] function, we can build an [OrderedType] structure. *) -Module NZOrderedTypeFunct (NZ : NZDecOrdSig') - <: DecidableTypeFull <: OrderedTypeFull := - NZ <+ NZOrderPropFunct <+ Compare2EqBool <+ HasEqBool2Dec. +Module NZOrderedType (NZ : NZDecOrdSig') + <: DecidableTypeFull <: OrderedTypeFull + := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v new file mode 100644 index 000000000..cbc286fbb --- /dev/null +++ b/theories/Numbers/NatInt/NZPow.v @@ -0,0 +1,358 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Power Function *) + +Require Import NZAxioms NZMulOrder. + +(** Interface of a power function, then its specification on naturals *) + +Module Type Pow (Import T:Typ). + Parameters Inline pow : t -> t -> t. +End Pow. + +Module Type PowNotation (T:Typ)(Import NZ:Pow T). + Infix "^" := pow. +End PowNotation. + +Module Type Pow' (T:Typ) := Pow T <+ PowNotation T. + +Module Type NZPowSpec (Import NZ : NZOrdAxiomsSig')(Import P : Pow' NZ). + Declare Instance pow_wd : Proper (eq==>eq==>eq) pow. + Axiom pow_0_r : forall a, a^0 == 1. + Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. +End NZPowSpec. + +Module Type NZPow (NZ:NZOrdAxiomsSig) := Pow NZ <+ NZPowSpec NZ. +Module Type NZPow' (NZ:NZOrdAxiomsSig) := Pow' NZ <+ NZPowSpec NZ. + +(** Derived properties of power *) + +Module NZPowProp + (Import NZ : NZOrdAxiomsSig') + (Import NZP : NZMulOrderProp NZ) + (Import NZP' : NZPow' NZ). + +Hint Rewrite pow_0_r pow_succ_r : nz. + +Lemma lt_0_2 : 0 < 2. +Proof. + apply lt_succ_r, le_0_1. +Qed. + +Ltac order' := generalize lt_0_1 lt_0_2; order. + +(** Power and basic constants *) + +Lemma pow_0_l : forall a, 0<a -> 0^a == 0. +Proof. + intros a Ha. + destruct (lt_exists_pred _ _ Ha) as (a' & EQ & Ha'). + rewrite EQ. now nzsimpl. +Qed. + +Lemma pow_1_r : forall a, a^1 == a. +Proof. + intros. now nzsimpl. +Qed. + +Lemma pow_1_l : forall a, 0<=a -> 1^a == 1. +Proof. + apply le_ind; intros. solve_predicate_wd. + now nzsimpl. + now nzsimpl. +Qed. + +Hint Rewrite pow_1_l : nz. + +Lemma pow_2_r : forall a, a^2 == a*a. +Proof. + intros. nzsimpl; order'. +Qed. + +(** Power and addition, multiplication *) + +Lemma pow_add_r : forall a b c, 0<=b -> 0<=c -> + a^(b+c) == a^b * a^c. +Proof. + intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + now nzsimpl. + clear b Hb. intros b Hb IH Hc. + nzsimpl; trivial. + rewrite IH; trivial. apply mul_assoc. + now apply add_nonneg_nonneg. +Qed. + +Lemma pow_mul_l : forall a b c, 0<=c -> + (a*b)^c == a^c * b^c. +Proof. + intros a b c Hc. apply le_ind with (4:=Hc). solve_predicate_wd. + now nzsimpl. + clear c Hc. intros c Hc IH. + nzsimpl; trivial. + rewrite IH; trivial. apply mul_shuffle1. +Qed. + +Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c -> + a^(b*c) == (a^b)^c. +Proof. + intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + intros. now nzsimpl. + clear b Hb. intros b Hb IH Hc. + nzsimpl; trivial. + rewrite pow_add_r, IH, pow_mul_l; trivial. apply mul_comm. + now apply mul_nonneg_nonneg. +Qed. + +(** Positivity *) + +Lemma pow_nonneg_nonneg : forall a b, 0<=a -> 0<=b -> 0<=a^b. +Proof. + intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + nzsimpl; order'. + clear b Hb. intros b Hb IH. + nzsimpl; trivial. now apply mul_nonneg_nonneg. +Qed. + +Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b. +Proof. + intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + nzsimpl; order'. + clear b Hb. intros b Hb IH. + nzsimpl; trivial. now apply mul_pos_pos. +Qed. + +(** Monotonicity *) + +Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c. +Proof. + intros a b c Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + intros (Ha,H). nzsimpl; trivial; order. + clear c Hc. intros c Hc IH (Ha,H). + nzsimpl; try order. + apply mul_lt_mono_nonneg; trivial. + apply pow_nonneg_nonneg; try order. + apply IH. now split. +Qed. + +Lemma pow_le_mono_l : forall a b c, 0<=c -> 0<=a<=b -> a^c <= b^c. +Proof. + intros a b c Hc (Ha,H). + apply lt_eq_cases in Hc; destruct Hc as [Hc|Hc]; [|rewrite <- Hc]. + apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H]. + apply lt_le_incl, pow_lt_mono_l; now try split. + now nzsimpl. +Qed. + +Lemma pow_gt_1 : forall a b, 1<a -> 0<b -> 1<a^b. +Proof. + intros a b Ha Hb. rewrite <- (pow_1_l b) by order. + apply pow_lt_mono_l; try split; order'. +Qed. + +Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=b<c -> a^b < a^c. +Proof. + intros a b c Ha (Hb,H). + assert (H' : b<=c) by order. + destruct (le_exists_sub _ _ H') as (d & EQ & Hd). + rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1. + apply mul_lt_mono_pos_r. + apply pow_pos_nonneg; order'. + apply pow_gt_1; trivial. + apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial. + rewrite <- EQ' in *. rewrite add_0_l in EQ. order. +Qed. + +(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *) + +Lemma pow_le_mono_r : forall a b c, 0<a -> 0<=b<=c -> a^b <= a^c. +Proof. + intros a b c Ha (Hb,H). + apply le_succ_l in Ha. + apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. + apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. + apply lt_le_incl, pow_lt_mono_r; now try split. + nzsimpl; order. +Qed. + +Lemma pow_le_mono : forall a b c d, 0<a<=c -> 0<=b<=d -> + a^b <= c^d. +Proof. + intros. transitivity (a^d). + apply pow_le_mono_r; intuition order. + apply pow_le_mono_l; intuition order. +Qed. + +Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> + a^b < c^d. +Proof. + intros a b c d (Ha,Hac) (Hb,Hbd). + apply le_succ_l in Ha. + apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. + transitivity (a^d). + apply pow_lt_mono_r; intuition order. + apply pow_lt_mono_l; try split; order'. + nzsimpl; try order. apply pow_gt_1; order. +Qed. + +(** Injectivity *) + +Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0<c -> + a^c == b^c -> a == b. +Proof. + intros a b c Ha Hb Hc EQ. + destruct (lt_trichotomy a b) as [LT|[EQ'|GT]]; trivial. + assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial). + order. + assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). + order. +Qed. + +Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c -> + a^b == a^c -> b == c. +Proof. + intros a b c Ha Hb Hc EQ. + destruct (lt_trichotomy b c) as [LT|[EQ'|GT]]; trivial. + assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial). + order. + assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial). + order. +Qed. + +(** Monotonicity results, both ways *) + +Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> + (a<b <-> a^c < b^c). +Proof. + intros a b c Ha Hb Hc. + split; intro LT. + apply pow_lt_mono_l; try split; trivial. + destruct (le_gt_cases b a) as [LE|GT]; trivial. + assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order). + order. +Qed. + +Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> + (a<=b <-> a^c <= b^c). +Proof. + intros a b c Ha Hb Hc. + split; intro LE. + apply pow_le_mono_l; try split; trivial. order. + destruct (le_gt_cases a b) as [LE'|GT]; trivial. + assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). + order. +Qed. + +Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c -> + (b<c <-> a^b < a^c). +Proof. + intros a b c Ha Hb Hc. + split; intro LT. + apply pow_lt_mono_r; try split; trivial. + destruct (le_gt_cases c b) as [LE|GT]; trivial. + assert (a^c <= a^b) by (apply pow_le_mono_r; try split; order'). + order. +Qed. + +Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c -> + (b<=c <-> a^b <= a^c). +Proof. + intros a b c Ha Hb Hc. + split; intro LE. + apply pow_le_mono_r; try split; trivial. order'. + destruct (le_gt_cases b c) as [LE'|GT]; trivial. + assert (a^c < a^b) by (apply pow_lt_mono_r; try split; order'). + order. +Qed. + +(** For any a>1, the a^x function is above the identity function *) + +Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b. +Proof. + intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + nzsimpl. order'. + clear b Hb. intros b Hb IH. nzsimpl; trivial. + rewrite <- !le_succ_l in *. + transitivity (2*(S b)). + nzsimpl. rewrite <- 2 succ_le_mono. + rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + apply mul_le_mono_nonneg; trivial. + order'. + now apply lt_le_incl, lt_succ_r. +Qed. + +(** Someday, we should say something about the full Newton formula. + In the meantime, we can at least provide some inequalities about + (a+b)^c. +*) + +Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c -> + a^c + b^c <= (a+b)^c. +Proof. + intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + nzsimpl; order. + clear c Hc. intros c Hc IH. + assert (0<=c) by order'. + nzsimpl; trivial. + transitivity ((a+b)*(a^c + b^c)). + rewrite mul_add_distr_r, !mul_add_distr_l. + apply add_le_mono. + rewrite <- add_0_r at 1. apply add_le_mono_l. + apply mul_nonneg_nonneg; trivial. + apply pow_nonneg_nonneg; trivial. + rewrite <- add_0_l at 1. apply add_le_mono_r. + apply mul_nonneg_nonneg; trivial. + apply pow_nonneg_nonneg; trivial. + apply mul_le_mono_nonneg_l; trivial. + now apply add_nonneg_nonneg. +Qed. + +(** This upper bound can also be seen as a convexity proof for x^c : + image of (a+b)/2 is below the middle of the images of a and b +*) + +Lemma pow_add_upper : forall a b c, 0<=a -> 0<=b -> 0<c -> + (a+b)^c <= 2^(pred c) * (a^c + b^c). +Proof. + assert (aux : forall a b c, 0<=a<=b -> 0<c -> + (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)). + (* begin *) + intros a b c (Ha,H) Hc. + rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl. + rewrite <- !add_assoc. apply add_le_mono_l. + rewrite !add_assoc. apply add_le_mono_r. + destruct (le_exists_sub _ _ H) as (d & EQ & Hd). + rewrite EQ. + rewrite 2 mul_add_distr_r. + rewrite !add_assoc. apply add_le_mono_r. + rewrite add_comm. apply add_le_mono_l. + apply mul_le_mono_nonneg_l; trivial. + apply pow_le_mono_l; try split; order. + (* end *) + intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + nzsimpl; order. + clear c Hc. intros c Hc IH. + assert (0<=c) by order. + nzsimpl; trivial. + transitivity ((a+b)*(2^(pred c) * (a^c + b^c))). + apply mul_le_mono_nonneg_l; trivial. + now apply add_nonneg_nonneg. + rewrite mul_assoc. rewrite (mul_comm (a+b)). + assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order'). + assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l). + assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl; order). + rewrite EQ', <- !mul_assoc. + apply mul_le_mono_nonneg_l. + apply pow_nonneg_nonneg; order'. + destruct (le_gt_cases a b). + apply aux; try split; order'. + rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)). + apply aux; try split; order'. +Qed. + +End NZPowProp. diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v index 5ef304606..13c262337 100644 --- a/theories/Numbers/NatInt/NZProperties.v +++ b/theories/Numbers/NatInt/NZProperties.v @@ -11,8 +11,8 @@ Require Export NZAxioms NZMulOrder. (** This functor summarizes all known facts about NZ. - For the moment it is only an alias to [NZMulOrderPropFunct], which + For the moment it is only an alias to [NZMulOrderProp], which subsumes all others. *) -Module Type NZPropFunct := NZMulOrderPropSig. +Module Type NZProp := NZMulOrderProp. |