Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Power Function
Require Import NZAxioms NZMulOrder.
Interface of a power function, then its specification on naturals
Module Type Pow (Import A : Typ). Parameters Inline pow : t -> t -> t. End Pow. Module Type PowNotation (A : Typ)(Import B : Pow A). Infix "^" := pow. End PowNotation. Module Type Pow' (A : Typ) := Pow A <+ PowNotation A. Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A). 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. Axiom pow_neg_r : forall a b, b<0 -> a^b == 0. End NZPowSpec.
The above pow_neg_r specification is useless (and trivially
provable) for N. Having it here already allows deriving
some slightly more general statements.
Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A. Module Type NZPow' (A : NZOrdAxiomsSig) := Pow' A <+ NZPowSpec A.
Derived properties of power
Module Type NZPowProp (Import A : NZOrdAxiomsSig') (Import B : NZPow' A) (Import C : NZMulOrderProp A). Hint Rewrite pow_0_r pow_succ_r : nz.
Power and basic constants
forall a : t, 0 < a -> 0 ^ a == 0forall a : t, 0 < a -> 0 ^ a == 0a:tHa:0 < a0 ^ a == 0a:tHa:0 < aa':tEQ:a == S a'Ha':0 <= a'0 ^ a == 0now nzsimpl. Qed.a:tHa:0 < aa':tEQ:a == S a'Ha':0 <= a'0 ^ S a' == 0forall a : t, a ~= 0 -> 0 ^ a == 0forall a : t, a ~= 0 -> 0 ^ a == 0a:tHa:a ~= 00 ^ a == 0a:tHa:a ~= 0LT:a < 00 ^ a == 0a:tHa:a ~= 0GT:0 < a0 ^ a == 0now rewrite pow_neg_r.a:tHa:a ~= 0LT:a < 00 ^ a == 0now apply pow_0_l. Qed.a:tHa:a ~= 0GT:0 < a0 ^ a == 0forall a : t, a ^ 1 == aforall a : t, a ^ 1 == anow nzsimpl'. Qed.a:ta ^ 1 == aforall a : t, 0 <= a -> 1 ^ a == 1forall a : t, 0 <= a -> 1 ^ a == 1Proper (eq ==> iff) (fun m : t => 1 ^ m == 1)1 ^ 0 == 1m:tH:0 <= mH0:1 ^ m == 11 ^ S m == 1solve_proper.Proper (eq ==> iff) (fun m : t => 1 ^ m == 1)now nzsimpl.1 ^ 0 == 1now nzsimpl. Qed. Hint Rewrite pow_1_r pow_1_l : nz.m:tH:0 <= mH0:1 ^ m == 11 ^ S m == 1forall a : t, a ^ 2 == a * aforall a : t, a ^ 2 == a * aa:ta ^ 2 == a * anzsimpl; order'. Qed. Hint Rewrite pow_2_r : nz.a:ta ^ S 1 == a * a
Power and nullity
forall a b : t, 0 <= b -> a ^ b == 0 -> a == 0forall a b : t, 0 <= b -> a ^ b == 0 -> a == 0a, b:tHb:0 <= ba ^ b == 0 -> a == 0a, b:tHb:0 <= bProper (eq ==> iff) (fun b0 : t => a ^ b0 == 0 -> a == 0)a, b:tHb:0 <= ba ^ 0 == 0 -> a == 0a, b:tHb:0 <= bforall m : t, 0 <= m -> (a ^ m == 0 -> a == 0) -> a ^ S m == 0 -> a == 0solve_proper.a, b:tHb:0 <= bProper (eq ==> iff) (fun b0 : t => a ^ b0 == 0 -> a == 0)a, b:tHb:0 <= ba ^ 0 == 0 -> a == 0order'.a, b:tHb:0 <= b1 == 0 -> a == 0a, b:tHb:0 <= bforall m : t, 0 <= m -> (a ^ m == 0 -> a == 0) -> a ^ S m == 0 -> a == 0a:tforall m : t, 0 <= m -> (a ^ m == 0 -> a == 0) -> a ^ S m == 0 -> a == 0a, b:tHb:0 <= bIH:a ^ b == 0 -> a == 0a ^ S b == 0 -> a == 0a, b:tHb:0 <= bIH:a ^ b == 0 -> a == 0a * a ^ b == 0 -> a == 0a, b:tHb:0 <= bIH:a ^ b == 0 -> a == 0H:a * a ^ b == 0a == 0a, b:tHb:0 <= bIH:a ^ b == 0 -> a == 0H:a == 0 \/ a ^ b == 0a == 0now apply IH. Qed.a, b:tHb:0 <= bIH:a ^ b == 0 -> a == 0H:a ^ b == 0a == 0forall a b : t, a ~= 0 -> 0 <= b -> a ^ b ~= 0forall a b : t, a ~= 0 -> 0 <= b -> a ^ b ~= 0a, b:tHa:a ~= 0Hb:0 <= ba ^ b ~= 0now apply pow_eq_0 with b. Qed.a, b:tHb:0 <= bHa:a ^ b == 0a == 0forall a b : t, a ^ b == 0 <-> b < 0 \/ 0 < b /\ a == 0forall a b : t, a ^ b == 0 <-> b < 0 \/ 0 < b /\ a == 0a, b:ta ^ b == 0 <-> b < 0 \/ 0 < b /\ a == 0a, b:ta ^ b == 0 -> b < 0 \/ 0 < b /\ a == 0a, b:tb < 0 \/ 0 < b /\ a == 0 -> a ^ b == 0a, b:ta ^ b == 0 -> b < 0 \/ 0 < b /\ a == 0a, b:tH:a ^ b == 0b < 0 \/ 0 < b /\ a == 0a, b:tH:a ^ b == 0Hb:b < 0b < 0 \/ 0 < b /\ a == 0a, b:tH:a ^ b == 0Hb:b == 0b < 0 \/ 0 < b /\ a == 0a, b:tH:a ^ b == 0Hb:0 < bb < 0 \/ 0 < b /\ a == 0now left.a, b:tH:a ^ b == 0Hb:b < 0b < 0 \/ 0 < b /\ a == 0rewrite Hb, pow_0_r in H; order'.a, b:tH:a ^ b == 0Hb:b == 0b < 0 \/ 0 < b /\ a == 0a, b:tH:a ^ b == 0Hb:0 < bb < 0 \/ 0 < b /\ a == 0a, b:tH:a ^ b == 0Hb:0 < b0 < b /\ a == 0apply pow_eq_0 with b; order.a, b:tH:a ^ b == 0Hb:0 < ba == 0a, b:tb < 0 \/ 0 < b /\ a == 0 -> a ^ b == 0a, b:tHb:b < 0a ^ b == 0a, b:tHb:0 < bHa:a == 0a ^ b == 0now rewrite pow_neg_r.a, b:tHb:b < 0a ^ b == 0a, b:tHb:0 < bHa:a == 0a ^ b == 0a, b:tHb:0 < bHa:a == 00 ^ b == 0order. Qed.a, b:tHb:0 < bHa:a == 0b ~= 0
Power and addition, multiplication
forall a b c : t, 0 <= b -> 0 <= c -> a ^ (b + c) == a ^ b * a ^ cforall a b c : t, 0 <= b -> 0 <= c -> a ^ (b + c) == a ^ b * a ^ ca, b, c:tHb:0 <= b0 <= c -> a ^ (b + c) == a ^ b * a ^ ca, b, c:tHb:0 <= bProper (eq ==> iff) (fun b0 : t => 0 <= c -> a ^ (b0 + c) == a ^ b0 * a ^ c)a, b, c:tHb:0 <= b0 <= c -> a ^ (0 + c) == a ^ 0 * a ^ ca, b, c:tHb:0 <= bforall m : t, 0 <= m -> (0 <= c -> a ^ (m + c) == a ^ m * a ^ c) -> 0 <= c -> a ^ (S m + c) == a ^ S m * a ^ csolve_proper.a, b, c:tHb:0 <= bProper (eq ==> iff) (fun b0 : t => 0 <= c -> a ^ (b0 + c) == a ^ b0 * a ^ c)now nzsimpl.a, b, c:tHb:0 <= b0 <= c -> a ^ (0 + c) == a ^ 0 * a ^ ca, b, c:tHb:0 <= bforall m : t, 0 <= m -> (0 <= c -> a ^ (m + c) == a ^ m * a ^ c) -> 0 <= c -> a ^ (S m + c) == a ^ S m * a ^ ca, c:tforall m : t, 0 <= m -> (0 <= c -> a ^ (m + c) == a ^ m * a ^ c) -> 0 <= c -> a ^ (S m + c) == a ^ S m * a ^ ca, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b + c) == a ^ b * a ^ cHc:0 <= ca ^ (S b + c) == a ^ S b * a ^ ca, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b + c) == a ^ b * a ^ cHc:0 <= ca * a ^ (b + c) == a * a ^ b * a ^ ca, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b + c) == a ^ b * a ^ cHc:0 <= c0 <= b + ca, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b + c) == a ^ b * a ^ cHc:0 <= ca * a ^ (b + c) == a * a ^ b * a ^ capply mul_assoc.a, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b + c) == a ^ b * a ^ cHc:0 <= ca * (a ^ b * a ^ c) == a * a ^ b * a ^ cnow apply add_nonneg_nonneg. Qed.a, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b + c) == a ^ b * a ^ cHc:0 <= c0 <= b + cforall a b c : t, (a * b) ^ c == a ^ c * b ^ cforall a b c : t, (a * b) ^ c == a ^ c * b ^ ca, b, c:t(a * b) ^ c == a ^ c * b ^ ca, b, c:tHc:c < 0(a * b) ^ c == a ^ c * b ^ ca, b, c:tHc:0 <= c(a * b) ^ c == a ^ c * b ^ ca, b, c:tHc:c < 0(a * b) ^ c == a ^ c * b ^ cnow nzsimpl.a, b, c:tHc:c < 00 == 0 * 0a, b, c:tHc:0 <= c(a * b) ^ c == a ^ c * b ^ ca, b, c:tHc:0 <= cProper (eq ==> iff) (fun c0 : t => (a * b) ^ c0 == a ^ c0 * b ^ c0)a, b, c:tHc:0 <= c(a * b) ^ 0 == a ^ 0 * b ^ 0a, b, c:tHc:0 <= cforall m : t, 0 <= m -> (a * b) ^ m == a ^ m * b ^ m -> (a * b) ^ S m == a ^ S m * b ^ S msolve_proper.a, b, c:tHc:0 <= cProper (eq ==> iff) (fun c0 : t => (a * b) ^ c0 == a ^ c0 * b ^ c0)now nzsimpl.a, b, c:tHc:0 <= c(a * b) ^ 0 == a ^ 0 * b ^ 0a, b, c:tHc:0 <= cforall m : t, 0 <= m -> (a * b) ^ m == a ^ m * b ^ m -> (a * b) ^ S m == a ^ S m * b ^ S ma, b:tforall m : t, 0 <= m -> (a * b) ^ m == a ^ m * b ^ m -> (a * b) ^ S m == a ^ S m * b ^ S ma, b, c:tHc:0 <= cIH:(a * b) ^ c == a ^ c * b ^ c(a * b) ^ S c == a ^ S c * b ^ S ca, b, c:tHc:0 <= cIH:(a * b) ^ c == a ^ c * b ^ ca * b * (a * b) ^ c == a * a ^ c * (b * b ^ c)apply mul_shuffle1. Qed.a, b, c:tHc:0 <= cIH:(a * b) ^ c == a ^ c * b ^ ca * b * (a ^ c * b ^ c) == a * a ^ c * (b * b ^ c)forall a b c : t, 0 <= b -> 0 <= c -> a ^ (b * c) == (a ^ b) ^ cforall a b c : t, 0 <= b -> 0 <= c -> a ^ (b * c) == (a ^ b) ^ ca, b, c:tHb:0 <= b0 <= c -> a ^ (b * c) == (a ^ b) ^ ca, b, c:tHb:0 <= bProper (eq ==> iff) (fun b0 : t => 0 <= c -> a ^ (b0 * c) == (a ^ b0) ^ c)a, b, c:tHb:0 <= b0 <= c -> a ^ (0 * c) == (a ^ 0) ^ ca, b, c:tHb:0 <= bforall m : t, 0 <= m -> (0 <= c -> a ^ (m * c) == (a ^ m) ^ c) -> 0 <= c -> a ^ (S m * c) == (a ^ S m) ^ csolve_proper.a, b, c:tHb:0 <= bProper (eq ==> iff) (fun b0 : t => 0 <= c -> a ^ (b0 * c) == (a ^ b0) ^ c)a, b, c:tHb:0 <= b0 <= c -> a ^ (0 * c) == (a ^ 0) ^ cnow nzsimpl.a, b, c:tHb:0 <= bH:0 <= ca ^ (0 * c) == (a ^ 0) ^ ca, b, c:tHb:0 <= bforall m : t, 0 <= m -> (0 <= c -> a ^ (m * c) == (a ^ m) ^ c) -> 0 <= c -> a ^ (S m * c) == (a ^ S m) ^ ca, c:tforall m : t, 0 <= m -> (0 <= c -> a ^ (m * c) == (a ^ m) ^ c) -> 0 <= c -> a ^ (S m * c) == (a ^ S m) ^ ca, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b * c) == (a ^ b) ^ cHc:0 <= ca ^ (S b * c) == (a ^ S b) ^ ca, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b * c) == (a ^ b) ^ cHc:0 <= ca ^ (b * c + c) == (a * a ^ b) ^ ca, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b * c) == (a ^ b) ^ cHc:0 <= c(a ^ b) ^ c * a ^ c == a ^ c * (a ^ b) ^ ca, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b * c) == (a ^ b) ^ cHc:0 <= c0 <= b * capply mul_comm.a, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b * c) == (a ^ b) ^ cHc:0 <= c(a ^ b) ^ c * a ^ c == a ^ c * (a ^ b) ^ cnow apply mul_nonneg_nonneg. Qed.a, c, b:tHb:0 <= bIH:0 <= c -> a ^ (b * c) == (a ^ b) ^ cHc:0 <= c0 <= b * c
Positivity
forall a b : t, 0 <= a -> 0 <= a ^ bforall a b : t, 0 <= a -> 0 <= a ^ ba, b:tHa:0 <= a0 <= a ^ ba, b:tHa:0 <= aHb:b < 00 <= a ^ ba, b:tHa:0 <= aHb:0 <= b0 <= a ^ bnow rewrite !(pow_neg_r _ _ Hb).a, b:tHa:0 <= aHb:b < 00 <= a ^ ba, b:tHa:0 <= aHb:0 <= b0 <= a ^ ba, b:tHa:0 <= aHb:0 <= bProper (eq ==> iff) (fun b0 : t => 0 <= a ^ b0)a, b:tHa:0 <= aHb:0 <= b0 <= a ^ 0a, b:tHa:0 <= aHb:0 <= bforall m : t, 0 <= m -> 0 <= a ^ m -> 0 <= a ^ S msolve_proper.a, b:tHa:0 <= aHb:0 <= bProper (eq ==> iff) (fun b0 : t => 0 <= a ^ b0)nzsimpl; order'.a, b:tHa:0 <= aHb:0 <= b0 <= a ^ 0a, b:tHa:0 <= aHb:0 <= bforall m : t, 0 <= m -> 0 <= a ^ m -> 0 <= a ^ S ma:tHa:0 <= aforall m : t, 0 <= m -> 0 <= a ^ m -> 0 <= a ^ S ma:tHa:0 <= ab:tHb:0 <= bIH:0 <= a ^ b0 <= a ^ S bnow apply mul_nonneg_nonneg. Qed.a:tHa:0 <= ab:tHb:0 <= bIH:0 <= a ^ b0 <= a * a ^ bforall a b : t, 0 < a -> 0 <= b -> 0 < a ^ bforall a b : t, 0 < a -> 0 <= b -> 0 < a ^ ba, b:tHa:0 < aHb:0 <= b0 < a ^ ba, b:tHa:0 < aHb:0 <= bProper (eq ==> iff) (fun b0 : t => 0 < a ^ b0)a, b:tHa:0 < aHb:0 <= b0 < a ^ 0a, b:tHa:0 < aHb:0 <= bforall m : t, 0 <= m -> 0 < a ^ m -> 0 < a ^ S msolve_proper.a, b:tHa:0 < aHb:0 <= bProper (eq ==> iff) (fun b0 : t => 0 < a ^ b0)nzsimpl; order'.a, b:tHa:0 < aHb:0 <= b0 < a ^ 0a, b:tHa:0 < aHb:0 <= bforall m : t, 0 <= m -> 0 < a ^ m -> 0 < a ^ S ma:tHa:0 < aforall m : t, 0 <= m -> 0 < a ^ m -> 0 < a ^ S ma:tHa:0 < ab:tHb:0 <= bIH:0 < a ^ b0 < a ^ S bnow apply mul_pos_pos. Qed.a:tHa:0 < ab:tHb:0 <= bIH:0 < a ^ b0 < a * a ^ b
Monotonicity
forall a b c : t, 0 < c -> 0 <= a < b -> a ^ c < b ^ cforall a b c : t, 0 < c -> 0 <= a < b -> a ^ c < b ^ ca, b, c:tHc:0 < c0 <= a < b -> a ^ c < b ^ ca, b, c:tHc:0 < cProper (eq ==> iff) (fun c0 : t => 0 <= a < b -> a ^ c0 < b ^ c0)a, b, c:tHc:0 < c0 <= a < b -> a ^ S 0 < b ^ S 0a, b, c:tHc:0 < cforall m : t, 0 < m -> (0 <= a < b -> a ^ m < b ^ m) -> 0 <= a < b -> a ^ S m < b ^ S msolve_proper.a, b, c:tHc:0 < cProper (eq ==> iff) (fun c0 : t => 0 <= a < b -> a ^ c0 < b ^ c0)a, b, c:tHc:0 < c0 <= a < b -> a ^ S 0 < b ^ S 0nzsimpl; trivial; order.a, b, c:tHc:0 < cHa:0 <= aH:a < ba ^ S 0 < b ^ S 0a, b, c:tHc:0 < cforall m : t, 0 < m -> (0 <= a < b -> a ^ m < b ^ m) -> 0 <= a < b -> a ^ S m < b ^ S ma, b:tforall m : t, 0 < m -> (0 <= a < b -> a ^ m < b ^ m) -> 0 <= a < b -> a ^ S m < b ^ S ma, b, c:tHc:0 < cIH:0 <= a < b -> a ^ c < b ^ cHa:0 <= aH:a < ba ^ S c < b ^ S ca, b, c:tHc:0 < cIH:0 <= a < b -> a ^ c < b ^ cHa:0 <= aH:a < ba * a ^ c < b * b ^ ca, b, c:tHc:0 < cIH:0 <= a < b -> a ^ c < b ^ cHa:0 <= aH:a < b0 <= a ^ ca, b, c:tHc:0 < cIH:0 <= a < b -> a ^ c < b ^ cHa:0 <= aH:a < ba ^ c < b ^ capply pow_nonneg; try order.a, b, c:tHc:0 < cIH:0 <= a < b -> a ^ c < b ^ cHa:0 <= aH:a < b0 <= a ^ ca, b, c:tHc:0 < cIH:0 <= a < b -> a ^ c < b ^ cHa:0 <= aH:a < ba ^ c < b ^ cnow split. Qed.a, b, c:tHc:0 < cIH:0 <= a < b -> a ^ c < b ^ cHa:0 <= aH:a < b0 <= a < bforall a b c : t, 0 <= a <= b -> a ^ c <= b ^ cforall a b c : t, 0 <= a <= b -> a ^ c <= b ^ ca, b, c:tHa:0 <= aH:a <= ba ^ c <= b ^ ca, b, c:tHa:0 <= aH:a <= bHc:c < 0a ^ c <= b ^ ca, b, c:tHa:0 <= aH:a <= bHc:c == 0a ^ c <= b ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < ca ^ c <= b ^ crewrite !(pow_neg_r _ _ Hc); now nzsimpl.a, b, c:tHa:0 <= aH:a <= bHc:c < 0a ^ c <= b ^ crewrite Hc; now nzsimpl.a, b, c:tHa:0 <= aH:a <= bHc:c == 0a ^ c <= b ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < ca ^ c <= b ^ ca, b, c:tHa:0 <= aH:a < b \/ a == bHc:0 < ca ^ c <= b ^ capply lt_le_incl, pow_lt_mono_l; now try split. Qed.a, b, c:tHa:0 <= aH:a < bHc:0 < ca ^ c <= b ^ cforall a b : t, 1 < a -> 0 < b <-> 1 < a ^ bforall a b : t, 1 < a -> 0 < b <-> 1 < a ^ ba, b:tHa:1 < a0 < b <-> 1 < a ^ ba, b:tHa:1 < aHb:0 < b1 < a ^ ba, b:tHa:1 < aHb:1 < a ^ b0 < ba, b:tHa:1 < aHb:0 < b1 < a ^ bapply pow_lt_mono_l; try split; order'.a, b:tHa:1 < aHb:0 < b1 ^ b < a ^ ba, b:tHa:1 < aHb:1 < a ^ b0 < ba, b:tHa:1 < aHb:1 < a ^ bH:b < 00 < ba, b:tHa:1 < aHb:1 < a ^ bH:b == 00 < brewrite pow_neg_r in Hb; order'.a, b:tHa:1 < aHb:1 < a ^ bH:b < 00 < ba, b:tHa:1 < aHb:1 < a ^ bH:b == 00 < border. Qed.a, b:tHa:1 < aHb:1 < 1H:b == 00 < bforall a b c : t, 1 < a -> 0 <= c -> b < c -> a ^ b < a ^ cforall a b c : t, 1 < a -> 0 <= c -> b < c -> a ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cH:b < ca ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cH:b < cHb:b < 0a ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= ba ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cH:b < cHb:b < 0a ^ b < a ^ capply pow_pos_nonneg; order'.a, b, c:tHa:1 < aHc:0 <= cH:b < cHb:b < 00 < a ^ ca, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= ba ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= ca ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bHd:0 <= da ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bHd:0 <= da ^ b < a ^ d * a ^ ba, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bHd:0 <= d1 * a ^ b < a ^ d * a ^ ba, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bHd:0 <= d0 < a ^ ba, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bHd:0 <= d1 < a ^ dapply pow_pos_nonneg; order'.a, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bHd:0 <= d0 < a ^ ba, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bHd:0 <= d1 < a ^ da, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bHd:0 <= d0 < da, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == d + bEQ':0 == d0 < da, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == 0 + bEQ':0 == d0 < 0order. Qed.a, b, c:tHa:1 < aHc:0 <= cH:b < cHb:0 <= bH':b <= cd:tEQ:c == bEQ':0 == d0 < 0
NB: since 0^0 > 0^1, the following result isn't valid with a=0
forall a b c : t, 0 < a -> b <= c -> a ^ b <= a ^ cforall a b c : t, 0 < a -> b <= c -> a ^ b <= a ^ ca, b, c:tHa:0 < aH:b <= ca ^ b <= a ^ ca, b, c:tHa:0 < aH:b <= cHb:b < 0a ^ b <= a ^ ca, b, c:tHa:0 < aH:b <= cHb:0 <= ba ^ b <= a ^ ca, b, c:tHa:0 < aH:b <= cHb:b < 0a ^ b <= a ^ capply pow_nonneg; order.a, b, c:tHa:0 < aH:b <= cHb:b < 00 <= a ^ ca, b, c:tHa:0 < aH:b <= cHb:0 <= ba ^ b <= a ^ ca, b, c:tHa:1 <= aH:b <= cHb:0 <= ba ^ b <= a ^ ca, b, c:tHa:1 < aH:b <= cHb:0 <= ba ^ b <= a ^ ca, b, c:tHa:1 == aH:b <= cHb:0 <= b1 ^ b <= 1 ^ ca, b, c:tHa:1 < aH:b <= cHb:0 <= ba ^ b <= a ^ capply lt_le_incl, pow_lt_mono_r; order.a, b, c:tHa:1 < aH:b < cHb:0 <= ba ^ b <= a ^ cnzsimpl; order. Qed.a, b, c:tHa:1 == aH:b <= cHb:0 <= b1 ^ b <= 1 ^ cforall a b c d : t, 0 < a <= c -> b <= d -> a ^ b <= c ^ dforall a b c d : t, 0 < a <= c -> b <= d -> a ^ b <= c ^ da, b, c, d:tH:0 < a <= cH0:b <= da ^ b <= c ^ da, b, c, d:tH:0 < a <= cH0:b <= da ^ b <= a ^ da, b, c, d:tH:0 < a <= cH0:b <= da ^ d <= c ^ dapply pow_le_mono_r; intuition order.a, b, c, d:tH:0 < a <= cH0:b <= da ^ b <= a ^ dapply pow_le_mono_l; intuition order. Qed.a, b, c, d:tH:0 < a <= cH0:b <= da ^ d <= c ^ dforall a b c d : t, 0 < a < c -> 0 < b < d -> a ^ b < c ^ dforall a b c d : t, 0 < a < c -> 0 < b < d -> a ^ b < c ^ da, b, c, d:tHa:0 < aHac:a < cHb:0 < bHbd:b < da ^ b < c ^ da, b, c, d:tHa:1 <= aHac:a < cHb:0 < bHbd:b < da ^ b < c ^ da, b, c, d:tHa:1 < aHac:a < cHb:0 < bHbd:b < da ^ b < c ^ da, b, c, d:tHa:1 == aHac:a < cHb:0 < bHbd:b < d1 ^ b < c ^ da, b, c, d:tHa:1 < aHac:a < cHb:0 < bHbd:b < da ^ b < c ^ da, b, c, d:tHa:1 < aHac:a < cHb:0 < bHbd:b < da ^ b < a ^ da, b, c, d:tHa:1 < aHac:a < cHb:0 < bHbd:b < da ^ d < c ^ dapply pow_lt_mono_r; intuition order.a, b, c, d:tHa:1 < aHac:a < cHb:0 < bHbd:b < da ^ b < a ^ dapply pow_lt_mono_l; try split; order'.a, b, c, d:tHa:1 < aHac:a < cHb:0 < bHbd:b < da ^ d < c ^ da, b, c, d:tHa:1 == aHac:a < cHb:0 < bHbd:b < d1 ^ b < c ^ dapply pow_gt_1; order. Qed.a, b, c, d:tHa:1 == aHac:a < cHb:0 < bHbd:b < d1 < c ^ d
Injectivity
forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a ^ c == b ^ c -> a == bforall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a ^ c == b ^ c -> a == ba, b, c:tHa:0 <= aHb:0 <= bHc:0 < cEQ:a ^ c == b ^ ca == ba, b, c:tHa:0 <= aHb:0 <= bHc:0 < cEQ:a ^ c == b ^ cLT:a < ba == ba, b, c:tHa:0 <= aHb:0 <= bHc:0 < cEQ:a ^ c == b ^ cGT:b < aa == ba, b, c:tHa:0 <= aHb:0 <= bHc:0 < cEQ:a ^ c == b ^ cLT:a < ba == border.a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cEQ:a ^ c == b ^ cLT:a < bH:a ^ c < b ^ ca == ba, b, c:tHa:0 <= aHb:0 <= bHc:0 < cEQ:a ^ c == b ^ cGT:b < aa == border. Qed.a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cEQ:a ^ c == b ^ cGT:b < aH:b ^ c < a ^ ca == bforall a b c : t, 1 < a -> 0 <= b -> 0 <= c -> a ^ b == a ^ c -> b == cforall a b c : t, 1 < a -> 0 <= b -> 0 <= c -> a ^ b == a ^ c -> b == ca, b, c:tHa:1 < aHb:0 <= bHc:0 <= cEQ:a ^ b == a ^ cb == ca, b, c:tHa:1 < aHb:0 <= bHc:0 <= cEQ:a ^ b == a ^ cLT:b < cb == ca, b, c:tHa:1 < aHb:0 <= bHc:0 <= cEQ:a ^ b == a ^ cGT:c < bb == ca, b, c:tHa:1 < aHb:0 <= bHc:0 <= cEQ:a ^ b == a ^ cLT:b < cb == corder.a, b, c:tHa:1 < aHb:0 <= bHc:0 <= cEQ:a ^ b == a ^ cLT:b < cH:a ^ b < a ^ cb == ca, b, c:tHa:1 < aHb:0 <= bHc:0 <= cEQ:a ^ b == a ^ cGT:c < bb == corder. Qed.a, b, c:tHa:1 < aHb:0 <= bHc:0 <= cEQ:a ^ b == a ^ cGT:c < bH:a ^ c < a ^ bb == c
Monotonicity results, both ways
forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a < b <-> a ^ c < b ^ cforall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a < b <-> a ^ c < b ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < ca < b <-> a ^ c < b ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLT:a < ba ^ c < b ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLT:a ^ c < b ^ ca < bapply pow_lt_mono_l; try split; trivial.a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLT:a < ba ^ c < b ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLT:a ^ c < b ^ ca < ba, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLT:a ^ c < b ^ cLE:b <= aa < border. Qed.a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLT:a ^ c < b ^ cLE:b <= aH:b ^ c <= a ^ ca < bforall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a <= b <-> a ^ c <= b ^ cforall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a <= b <-> a ^ c <= b ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < ca <= b <-> a ^ c <= b ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLE:a <= ba ^ c <= b ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLE:a ^ c <= b ^ ca <= bapply pow_le_mono_l; try split; trivial.a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLE:a <= ba ^ c <= b ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLE:a ^ c <= b ^ ca <= ba, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLE:a ^ c <= b ^ cGT:b < aa <= border. Qed.a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cLE:a ^ c <= b ^ cGT:b < aH:b ^ c < a ^ ca <= bforall a b c : t, 1 < a -> 0 <= c -> b < c <-> a ^ b < a ^ cforall a b c : t, 1 < a -> 0 <= c -> b < c <-> a ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cb < c <-> a ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cLT:b < ca ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cLT:a ^ b < a ^ cb < cnow apply pow_lt_mono_r.a, b, c:tHa:1 < aHc:0 <= cLT:b < ca ^ b < a ^ ca, b, c:tHa:1 < aHc:0 <= cLT:a ^ b < a ^ cb < ca, b, c:tHa:1 < aHc:0 <= cLT:a ^ b < a ^ cLE:c <= bb < corder. Qed.a, b, c:tHa:1 < aHc:0 <= cLT:a ^ b < a ^ cLE:c <= bH:a ^ c <= a ^ bb < cforall a b c : t, 1 < a -> 0 <= c -> b <= c <-> a ^ b <= a ^ cforall a b c : t, 1 < a -> 0 <= c -> b <= c <-> a ^ b <= a ^ ca, b, c:tHa:1 < aHc:0 <= cb <= c <-> a ^ b <= a ^ ca, b, c:tHa:1 < aHc:0 <= cLE:b <= ca ^ b <= a ^ ca, b, c:tHa:1 < aHc:0 <= cLE:a ^ b <= a ^ cb <= capply pow_le_mono_r; order'.a, b, c:tHa:1 < aHc:0 <= cLE:b <= ca ^ b <= a ^ ca, b, c:tHa:1 < aHc:0 <= cLE:a ^ b <= a ^ cb <= ca, b, c:tHa:1 < aHc:0 <= cLE:a ^ b <= a ^ cGT:c < bb <= corder. Qed.a, b, c:tHa:1 < aHc:0 <= cLE:a ^ b <= a ^ cGT:c < bH:a ^ c < a ^ bb <= c
For any a>1, the a^x function is above the identity function
forall a b : t, 1 < a -> 0 <= b -> b < a ^ bforall a b : t, 1 < a -> 0 <= b -> b < a ^ ba, b:tHa:1 < aHb:0 <= bb < a ^ ba, b:tHa:1 < aHb:0 <= bProper (eq ==> iff) (fun b0 : t => b0 < a ^ b0)a, b:tHa:1 < aHb:0 <= b0 < a ^ 0a, b:tHa:1 < aHb:0 <= bforall m : t, 0 <= m -> m < a ^ m -> S m < a ^ S msolve_proper.a, b:tHa:1 < aHb:0 <= bProper (eq ==> iff) (fun b0 : t => b0 < a ^ b0)a, b:tHa:1 < aHb:0 <= b0 < a ^ 0order'.a, b:tHa:1 < aHb:0 <= b0 < 1a, b:tHa:1 < aHb:0 <= bforall m : t, 0 <= m -> m < a ^ m -> S m < a ^ S ma:tHa:1 < aforall m : t, 0 <= m -> m < a ^ m -> S m < a ^ S ma:tHa:1 < ab:tHb:0 <= bIH:b < a ^ bS b < a ^ S ba:tHa:1 < ab:tHb:0 <= bIH:b < a ^ bS b < a * a ^ ba:tHa:S 1 <= ab:tHb:0 <= bIH:S b <= a ^ bS (S b) <= a * a ^ ba:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ bS (S b) <= a * a ^ ba:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ bS (S b) <= 2 * S ba:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ b2 * S b <= a * a ^ ba:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ bS (S b) <= 2 * S ba:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ bS (S b) <= S (S (b + b))a:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ bb <= b + bapply add_le_mono; order.a:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ b0 + b <= b + ba:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ b2 * S b <= a * a ^ ba:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ b0 <= 2a:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ b0 <= S border'.a:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ b0 <= 2now apply lt_le_incl, lt_succ_r. Qed.a:tHa:2 <= ab:tHb:0 <= bIH:S b <= a ^ b0 <= S b
Someday, we should say something about the full Newton formula.
In the meantime, we can at least provide some inequalities about
(a+b)^c.
forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a ^ c + b ^ c <= (a + b) ^ cforall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a ^ c + b ^ c <= (a + b) ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < ca ^ c + b ^ c <= (a + b) ^ ca, b, c:tHa:0 <= aHb:0 <= bHc:0 < cProper (eq ==> iff) (fun c0 : t => a ^ c0 + b ^ c0 <= (a + b) ^ c0)a, b, c:tHa:0 <= aHb:0 <= bHc:0 < ca ^ S 0 + b ^ S 0 <= (a + b) ^ S 0a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cforall m : t, 0 < m -> a ^ m + b ^ m <= (a + b) ^ m -> a ^ S m + b ^ S m <= (a + b) ^ S msolve_proper.a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cProper (eq ==> iff) (fun c0 : t => a ^ c0 + b ^ c0 <= (a + b) ^ c0)nzsimpl; order.a, b, c:tHa:0 <= aHb:0 <= bHc:0 < ca ^ S 0 + b ^ S 0 <= (a + b) ^ S 0a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cforall m : t, 0 < m -> a ^ m + b ^ m <= (a + b) ^ m -> a ^ S m + b ^ S m <= (a + b) ^ S ma, b:tHa:0 <= aHb:0 <= bforall m : t, 0 < m -> a ^ m + b ^ m <= (a + b) ^ m -> a ^ S m + b ^ S m <= (a + b) ^ S ma, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ ca ^ S c + b ^ S c <= (a + b) ^ S ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= ca ^ S c + b ^ S c <= (a + b) ^ S ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= ca * a ^ c + b * b ^ c <= (a + b) * (a + b) ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= ca * a ^ c + b * b ^ c <= (a + b) * (a ^ c + b ^ c)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= c(a + b) * (a ^ c + b ^ c) <= (a + b) * (a + b) ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= ca * a ^ c + b * b ^ c <= (a + b) * (a ^ c + b ^ c)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= ca * a ^ c + b * b ^ c <= a * a ^ c + a * b ^ c + (b * a ^ c + b * b ^ c)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= ca * a ^ c <= a * a ^ c + a * b ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= cb * b ^ c <= b * a ^ c + b * b ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= ca * a ^ c <= a * a ^ c + a * b ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= ca * a ^ c + 0 <= a * a ^ c + a * b ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= c0 <= a * b ^ capply pow_nonneg; trivial.a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= c0 <= b ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= cb * b ^ c <= b * a ^ c + b * b ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= c0 + b * b ^ c <= b * a ^ c + b * b ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= c0 <= b * a ^ capply pow_nonneg; trivial.a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= c0 <= a ^ ca, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= c(a + b) * (a ^ c + b ^ c) <= (a + b) * (a + b) ^ cnow apply add_nonneg_nonneg. Qed.a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:a ^ c + b ^ c <= (a + b) ^ cH:0 <= c0 <= a + b
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
forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> (a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> (a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)(* begin *)forall a b c : t, 0 <= a <= b -> 0 < c -> (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)aux:forall a b c : t, 0 <= a <= b -> 0 < c -> (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> (a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)forall a b c : t, 0 <= a <= b -> 0 < c -> (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)a, b, c:tHa:0 <= aH:a <= bHc:0 < c(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)a, b, c:tHa:0 <= aH:a <= bHc:0 < ca * a ^ c + b * a ^ c + (a * b ^ c + b * b ^ c) <= 2 * (a * a ^ c) + 2 * (b * b ^ c)a, b, c:tHa:0 <= aH:a <= bHc:0 < ca * a ^ c + b * a ^ c + (a * b ^ c + b * b ^ c) <= a * a ^ c + a * a ^ c + (b * b ^ c + b * b ^ c)a, b, c:tHa:0 <= aH:a <= bHc:0 < ca * a ^ c + (b * a ^ c + (a * b ^ c + b * b ^ c)) <= a * a ^ c + (a * a ^ c + (b * b ^ c + b * b ^ c))a, b, c:tHa:0 <= aH:a <= bHc:0 < cb * a ^ c + (a * b ^ c + b * b ^ c) <= a * a ^ c + (b * b ^ c + b * b ^ c)a, b, c:tHa:0 <= aH:a <= bHc:0 < cb * a ^ c + a * b ^ c + b * b ^ c <= a * a ^ c + b * b ^ c + b * b ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < cb * a ^ c + a * b ^ c <= a * a ^ c + b * b ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < cd:tEQ:b == d + aHd:0 <= db * a ^ c + a * b ^ c <= a * a ^ c + b * b ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < cd:tEQ:b == d + aHd:0 <= d(d + a) * a ^ c + a * (d + a) ^ c <= a * a ^ c + (d + a) * (d + a) ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < cd:tEQ:b == d + aHd:0 <= dd * a ^ c + a * a ^ c + a * (d + a) ^ c <= a * a ^ c + (d * (d + a) ^ c + a * (d + a) ^ c)a, b, c:tHa:0 <= aH:a <= bHc:0 < cd:tEQ:b == d + aHd:0 <= dd * a ^ c + a * a ^ c + a * (d + a) ^ c <= a * a ^ c + d * (d + a) ^ c + a * (d + a) ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < cd:tEQ:b == d + aHd:0 <= dd * a ^ c + a * a ^ c <= a * a ^ c + d * (d + a) ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < cd:tEQ:b == d + aHd:0 <= da * a ^ c + d * a ^ c <= a * a ^ c + d * (d + a) ^ ca, b, c:tHa:0 <= aH:a <= bHc:0 < cd:tEQ:b == d + aHd:0 <= dd * a ^ c <= d * (d + a) ^ capply pow_le_mono_l; try split; order. (* end *)a, b, c:tHa:0 <= aH:a <= bHc:0 < cd:tEQ:b == d + aHd:0 <= da ^ c <= (d + a) ^ caux:forall a b c : t, 0 <= a <= b -> 0 < c -> (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> (a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b, c:tHa:0 <= aHb:0 <= bHc:0 < c(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cProper (eq ==> iff) (fun c0 : t => (a + b) ^ c0 <= 2 ^ P c0 * (a ^ c0 + b ^ c0))aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b, c:tHa:0 <= aHb:0 <= bHc:0 < c(a + b) ^ S 0 <= 2 ^ P (S 0) * (a ^ S 0 + b ^ S 0)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cforall m : t, 0 < m -> (a + b) ^ m <= 2 ^ P m * (a ^ m + b ^ m) -> (a + b) ^ S m <= 2 ^ P (S m) * (a ^ S m + b ^ S m)solve_proper.aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cProper (eq ==> iff) (fun c0 : t => (a + b) ^ c0 <= 2 ^ P c0 * (a ^ c0 + b ^ c0))nzsimpl; order.aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b, c:tHa:0 <= aHb:0 <= bHc:0 < c(a + b) ^ S 0 <= 2 ^ P (S 0) * (a ^ S 0 + b ^ S 0)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b, c:tHa:0 <= aHb:0 <= bHc:0 < cforall m : t, 0 < m -> (a + b) ^ m <= 2 ^ P m * (a ^ m + b ^ m) -> (a + b) ^ S m <= 2 ^ P (S m) * (a ^ S m + b ^ S m)aux:forall a0 b0 c : t, 0 <= a0 <= b0 -> 0 < c -> (a0 + b0) * (a0 ^ c + b0 ^ c) <= 2 * (a0 * a0 ^ c + b0 * b0 ^ c)a, b:tHa:0 <= aHb:0 <= bforall m : t, 0 < m -> (a + b) ^ m <= 2 ^ P m * (a ^ m + b ^ m) -> (a + b) ^ S m <= 2 ^ P (S m) * (a ^ S m + b ^ S m)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)(a + b) ^ S c <= 2 ^ P (S c) * (a ^ S c + b ^ S c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c(a + b) ^ S c <= 2 ^ P (S c) * (a ^ S c + b ^ S c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c(a + b) * (a + b) ^ c <= 2 ^ c * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c(a + b) * (a + b) ^ c <= (a + b) * (2 ^ P c * (a ^ c + b ^ c))aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c(a + b) * (2 ^ P c * (a ^ c + b ^ c)) <= 2 ^ c * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c(a + b) * (a + b) ^ c <= (a + b) * (2 ^ P c * (a ^ c + b ^ c))now apply add_nonneg_nonneg.aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c0 <= a + baux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c(a + b) * (2 ^ P c * (a ^ c + b ^ c)) <= 2 ^ c * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c(a + b) * 2 ^ P c * (a ^ c + b ^ c) <= 2 ^ c * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= c2 ^ P c * (a + b) * (a ^ c + b ^ c) <= 2 ^ c * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == c2 ^ P c * (a + b) * (a ^ c + b ^ c) <= 2 ^ c * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P c2 ^ P c * (a + b) * (a ^ c + b ^ c) <= 2 ^ c * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 22 ^ P c * (a + b) * (a ^ c + b ^ c) <= 2 ^ c * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 22 ^ P c * ((a + b) * (a ^ c + b ^ c)) <= 2 ^ P c * (2 * (a * a ^ c + b * b ^ c))aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 20 <= 2 ^ P caux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 2(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)apply pow_nonneg; order'.aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 20 <= 2 ^ P caux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 2(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 2H0:a <= b(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 2H0:b < a(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)apply aux; try split; order'.aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 2H0:a <= b(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 2H0:b < a(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)apply aux; try split; order'. Qed. End NZPowProp.aux:forall a0 b0 c0 : t, 0 <= a0 <= b0 -> 0 < c0 -> (a0 + b0) * (a0 ^ c0 + b0 ^ c0) <= 2 * (a0 * a0 ^ c0 + b0 * b0 ^ c0)a, b:tHa:0 <= aHb:0 <= bc:tHc:0 < cIH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)H:0 <= cEQ:S (P c) == cLE:0 <= P cEQ':2 ^ c == 2 ^ P c * 2H0:b < a(b + a) * (b ^ c + a ^ c) <= 2 * (b * b ^ c + a * a ^ c)