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 == 0

forall a : t, 0 < a -> 0 ^ a == 0
a:t
Ha:0 < a

0 ^ a == 0
a:t
Ha:0 < a
a':t
EQ:a == S a'
Ha':0 <= a'

0 ^ a == 0
a:t
Ha:0 < a
a':t
EQ:a == S a'
Ha':0 <= a'

0 ^ S a' == 0
now nzsimpl. Qed.

forall a : t, a ~= 0 -> 0 ^ a == 0

forall a : t, a ~= 0 -> 0 ^ a == 0
a:t
Ha:a ~= 0

0 ^ a == 0
a:t
Ha:a ~= 0
LT:a < 0

0 ^ a == 0
a:t
Ha:a ~= 0
GT:0 < a
0 ^ a == 0
a:t
Ha:a ~= 0
LT:a < 0

0 ^ a == 0
now rewrite pow_neg_r.
a:t
Ha:a ~= 0
GT:0 < a

0 ^ a == 0
now apply pow_0_l. Qed.

forall a : t, a ^ 1 == a

forall a : t, a ^ 1 == a
a:t

a ^ 1 == a
now nzsimpl'. Qed.

forall a : t, 0 <= a -> 1 ^ a == 1

forall a : t, 0 <= a -> 1 ^ a == 1

Proper (eq ==> iff) (fun m : t => 1 ^ m == 1)

1 ^ 0 == 1
m:t
H:0 <= m
H0:1 ^ m == 1
1 ^ S m == 1

Proper (eq ==> iff) (fun m : t => 1 ^ m == 1)
solve_proper.

1 ^ 0 == 1
now nzsimpl.
m:t
H:0 <= m
H0:1 ^ m == 1

1 ^ S m == 1
now nzsimpl. Qed. Hint Rewrite pow_1_r pow_1_l : nz.

forall a : t, a ^ 2 == a * a

forall a : t, a ^ 2 == a * a
a:t

a ^ 2 == a * a
a:t

a ^ S 1 == a * a
nzsimpl; order'. Qed. Hint Rewrite pow_2_r : nz.
Power and nullity

forall a b : t, 0 <= b -> a ^ b == 0 -> a == 0

forall a b : t, 0 <= b -> a ^ b == 0 -> a == 0
a, b:t
Hb:0 <= b

a ^ b == 0 -> a == 0
a, b:t
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => a ^ b0 == 0 -> a == 0)
a, b:t
Hb:0 <= b
a ^ 0 == 0 -> a == 0
a, b:t
Hb:0 <= b
forall m : t, 0 <= m -> (a ^ m == 0 -> a == 0) -> a ^ S m == 0 -> a == 0
a, b:t
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => a ^ b0 == 0 -> a == 0)
solve_proper.
a, b:t
Hb:0 <= b

a ^ 0 == 0 -> a == 0
a, b:t
Hb:0 <= b

1 == 0 -> a == 0
order'.
a, b:t
Hb:0 <= b

forall m : t, 0 <= m -> (a ^ m == 0 -> a == 0) -> a ^ S m == 0 -> a == 0
a:t

forall m : t, 0 <= m -> (a ^ m == 0 -> a == 0) -> a ^ S m == 0 -> a == 0
a, b:t
Hb:0 <= b
IH:a ^ b == 0 -> a == 0

a ^ S b == 0 -> a == 0
a, b:t
Hb:0 <= b
IH:a ^ b == 0 -> a == 0

a * a ^ b == 0 -> a == 0
a, b:t
Hb:0 <= b
IH:a ^ b == 0 -> a == 0
H:a * a ^ b == 0

a == 0
a, b:t
Hb:0 <= b
IH:a ^ b == 0 -> a == 0
H:a == 0 \/ a ^ b == 0

a == 0
a, b:t
Hb:0 <= b
IH:a ^ b == 0 -> a == 0
H:a ^ b == 0

a == 0
now apply IH. Qed.

forall a b : t, a ~= 0 -> 0 <= b -> a ^ b ~= 0

forall a b : t, a ~= 0 -> 0 <= b -> a ^ b ~= 0
a, b:t
Ha:a ~= 0
Hb:0 <= b

a ^ b ~= 0
a, b:t
Hb:0 <= b
Ha:a ^ b == 0

a == 0
now apply pow_eq_0 with b. Qed.

forall a b : t, a ^ b == 0 <-> b < 0 \/ 0 < b /\ a == 0

forall a b : t, a ^ b == 0 <-> b < 0 \/ 0 < b /\ a == 0
a, b:t

a ^ b == 0 <-> b < 0 \/ 0 < b /\ a == 0
a, b:t

a ^ b == 0 -> b < 0 \/ 0 < b /\ a == 0
a, b:t
b < 0 \/ 0 < b /\ a == 0 -> a ^ b == 0
a, b:t

a ^ b == 0 -> b < 0 \/ 0 < b /\ a == 0
a, b:t
H:a ^ b == 0

b < 0 \/ 0 < b /\ a == 0
a, b:t
H:a ^ b == 0
Hb:b < 0

b < 0 \/ 0 < b /\ a == 0
a, b:t
H:a ^ b == 0
Hb:b == 0
b < 0 \/ 0 < b /\ a == 0
a, b:t
H:a ^ b == 0
Hb:0 < b
b < 0 \/ 0 < b /\ a == 0
a, b:t
H:a ^ b == 0
Hb:b < 0

b < 0 \/ 0 < b /\ a == 0
now left.
a, b:t
H:a ^ b == 0
Hb:b == 0

b < 0 \/ 0 < b /\ a == 0
rewrite Hb, pow_0_r in H; order'.
a, b:t
H:a ^ b == 0
Hb:0 < b

b < 0 \/ 0 < b /\ a == 0
a, b:t
H:a ^ b == 0
Hb:0 < b

0 < b /\ a == 0
a, b:t
H:a ^ b == 0
Hb:0 < b

a == 0
apply pow_eq_0 with b; order.
a, b:t

b < 0 \/ 0 < b /\ a == 0 -> a ^ b == 0
a, b:t
Hb:b < 0

a ^ b == 0
a, b:t
Hb:0 < b
Ha:a == 0
a ^ b == 0
a, b:t
Hb:b < 0

a ^ b == 0
now rewrite pow_neg_r.
a, b:t
Hb:0 < b
Ha:a == 0

a ^ b == 0
a, b:t
Hb:0 < b
Ha:a == 0

0 ^ b == 0
a, b:t
Hb:0 < b
Ha:a == 0

b ~= 0
order. Qed.
Power and addition, multiplication

forall a b c : t, 0 <= b -> 0 <= c -> a ^ (b + c) == a ^ b * a ^ c

forall a b c : t, 0 <= b -> 0 <= c -> a ^ (b + c) == a ^ b * a ^ c
a, b, c:t
Hb:0 <= b

0 <= c -> a ^ (b + c) == a ^ b * a ^ c
a, b, c:t
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => 0 <= c -> a ^ (b0 + c) == a ^ b0 * a ^ c)
a, b, c:t
Hb:0 <= b
0 <= c -> a ^ (0 + c) == a ^ 0 * a ^ c
a, b, c:t
Hb:0 <= b
forall m : t, 0 <= m -> (0 <= c -> a ^ (m + c) == a ^ m * a ^ c) -> 0 <= c -> a ^ (S m + c) == a ^ S m * a ^ c
a, b, c:t
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => 0 <= c -> a ^ (b0 + c) == a ^ b0 * a ^ c)
solve_proper.
a, b, c:t
Hb:0 <= b

0 <= c -> a ^ (0 + c) == a ^ 0 * a ^ c
now nzsimpl.
a, b, c:t
Hb:0 <= b

forall m : t, 0 <= m -> (0 <= c -> a ^ (m + c) == a ^ m * a ^ c) -> 0 <= c -> a ^ (S m + c) == a ^ S m * a ^ c
a, c:t

forall m : t, 0 <= m -> (0 <= c -> a ^ (m + c) == a ^ m * a ^ c) -> 0 <= c -> a ^ (S m + c) == a ^ S m * a ^ c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b + c) == a ^ b * a ^ c
Hc:0 <= c

a ^ (S b + c) == a ^ S b * a ^ c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b + c) == a ^ b * a ^ c
Hc:0 <= c

a * a ^ (b + c) == a * a ^ b * a ^ c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b + c) == a ^ b * a ^ c
Hc:0 <= c
0 <= b + c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b + c) == a ^ b * a ^ c
Hc:0 <= c

a * a ^ (b + c) == a * a ^ b * a ^ c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b + c) == a ^ b * a ^ c
Hc:0 <= c

a * (a ^ b * a ^ c) == a * a ^ b * a ^ c
apply mul_assoc.
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b + c) == a ^ b * a ^ c
Hc:0 <= c

0 <= b + c
now apply add_nonneg_nonneg. Qed.

forall a b c : t, (a * b) ^ c == a ^ c * b ^ c

forall a b c : t, (a * b) ^ c == a ^ c * b ^ c
a, b, c:t

(a * b) ^ c == a ^ c * b ^ c
a, b, c:t
Hc:c < 0

(a * b) ^ c == a ^ c * b ^ c
a, b, c:t
Hc:0 <= c
(a * b) ^ c == a ^ c * b ^ c
a, b, c:t
Hc:c < 0

(a * b) ^ c == a ^ c * b ^ c
a, b, c:t
Hc:c < 0

0 == 0 * 0
now nzsimpl.
a, b, c:t
Hc:0 <= c

(a * b) ^ c == a ^ c * b ^ c
a, b, c:t
Hc:0 <= c

Proper (eq ==> iff) (fun c0 : t => (a * b) ^ c0 == a ^ c0 * b ^ c0)
a, b, c:t
Hc:0 <= c
(a * b) ^ 0 == a ^ 0 * b ^ 0
a, b, c:t
Hc:0 <= c
forall m : t, 0 <= m -> (a * b) ^ m == a ^ m * b ^ m -> (a * b) ^ S m == a ^ S m * b ^ S m
a, b, c:t
Hc:0 <= c

Proper (eq ==> iff) (fun c0 : t => (a * b) ^ c0 == a ^ c0 * b ^ c0)
solve_proper.
a, b, c:t
Hc:0 <= c

(a * b) ^ 0 == a ^ 0 * b ^ 0
now nzsimpl.
a, b, c:t
Hc:0 <= c

forall m : t, 0 <= m -> (a * b) ^ m == a ^ m * b ^ m -> (a * b) ^ S m == a ^ S m * b ^ S m
a, b:t

forall m : t, 0 <= m -> (a * b) ^ m == a ^ m * b ^ m -> (a * b) ^ S m == a ^ S m * b ^ S m
a, b, c:t
Hc:0 <= c
IH:(a * b) ^ c == a ^ c * b ^ c

(a * b) ^ S c == a ^ S c * b ^ S c
a, b, c:t
Hc:0 <= c
IH:(a * b) ^ c == a ^ c * b ^ c

a * b * (a * b) ^ c == a * a ^ c * (b * b ^ c)
a, b, c:t
Hc:0 <= c
IH:(a * b) ^ c == a ^ c * b ^ c

a * b * (a ^ c * b ^ c) == a * a ^ c * (b * b ^ c)
apply mul_shuffle1. Qed.

forall a b c : t, 0 <= b -> 0 <= c -> a ^ (b * c) == (a ^ b) ^ c

forall a b c : t, 0 <= b -> 0 <= c -> a ^ (b * c) == (a ^ b) ^ c
a, b, c:t
Hb:0 <= b

0 <= c -> a ^ (b * c) == (a ^ b) ^ c
a, b, c:t
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => 0 <= c -> a ^ (b0 * c) == (a ^ b0) ^ c)
a, b, c:t
Hb:0 <= b
0 <= c -> a ^ (0 * c) == (a ^ 0) ^ c
a, b, c:t
Hb:0 <= b
forall m : t, 0 <= m -> (0 <= c -> a ^ (m * c) == (a ^ m) ^ c) -> 0 <= c -> a ^ (S m * c) == (a ^ S m) ^ c
a, b, c:t
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => 0 <= c -> a ^ (b0 * c) == (a ^ b0) ^ c)
solve_proper.
a, b, c:t
Hb:0 <= b

0 <= c -> a ^ (0 * c) == (a ^ 0) ^ c
a, b, c:t
Hb:0 <= b
H:0 <= c

a ^ (0 * c) == (a ^ 0) ^ c
now nzsimpl.
a, b, c:t
Hb:0 <= b

forall m : t, 0 <= m -> (0 <= c -> a ^ (m * c) == (a ^ m) ^ c) -> 0 <= c -> a ^ (S m * c) == (a ^ S m) ^ c
a, c:t

forall m : t, 0 <= m -> (0 <= c -> a ^ (m * c) == (a ^ m) ^ c) -> 0 <= c -> a ^ (S m * c) == (a ^ S m) ^ c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b * c) == (a ^ b) ^ c
Hc:0 <= c

a ^ (S b * c) == (a ^ S b) ^ c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b * c) == (a ^ b) ^ c
Hc:0 <= c

a ^ (b * c + c) == (a * a ^ b) ^ c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b * c) == (a ^ b) ^ c
Hc:0 <= c

(a ^ b) ^ c * a ^ c == a ^ c * (a ^ b) ^ c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b * c) == (a ^ b) ^ c
Hc:0 <= c
0 <= b * c
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b * c) == (a ^ b) ^ c
Hc:0 <= c

(a ^ b) ^ c * a ^ c == a ^ c * (a ^ b) ^ c
apply mul_comm.
a, c, b:t
Hb:0 <= b
IH:0 <= c -> a ^ (b * c) == (a ^ b) ^ c
Hc:0 <= c

0 <= b * c
now apply mul_nonneg_nonneg. Qed.
Positivity

forall a b : t, 0 <= a -> 0 <= a ^ b

forall a b : t, 0 <= a -> 0 <= a ^ b
a, b:t
Ha:0 <= a

0 <= a ^ b
a, b:t
Ha:0 <= a
Hb:b < 0

0 <= a ^ b
a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= a ^ b
a, b:t
Ha:0 <= a
Hb:b < 0

0 <= a ^ b
now rewrite !(pow_neg_r _ _ Hb).
a, b:t
Ha:0 <= a
Hb:0 <= b

0 <= a ^ b
a, b:t
Ha:0 <= a
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => 0 <= a ^ b0)
a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= a ^ 0
a, b:t
Ha:0 <= a
Hb:0 <= b
forall m : t, 0 <= m -> 0 <= a ^ m -> 0 <= a ^ S m
a, b:t
Ha:0 <= a
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => 0 <= a ^ b0)
solve_proper.
a, b:t
Ha:0 <= a
Hb:0 <= b

0 <= a ^ 0
nzsimpl; order'.
a, b:t
Ha:0 <= a
Hb:0 <= b

forall m : t, 0 <= m -> 0 <= a ^ m -> 0 <= a ^ S m
a:t
Ha:0 <= a

forall m : t, 0 <= m -> 0 <= a ^ m -> 0 <= a ^ S m
a:t
Ha:0 <= a
b:t
Hb:0 <= b
IH:0 <= a ^ b

0 <= a ^ S b
a:t
Ha:0 <= a
b:t
Hb:0 <= b
IH:0 <= a ^ b

0 <= a * a ^ b
now apply mul_nonneg_nonneg. Qed.

forall a b : t, 0 < a -> 0 <= b -> 0 < a ^ b

forall a b : t, 0 < a -> 0 <= b -> 0 < a ^ b
a, b:t
Ha:0 < a
Hb:0 <= b

0 < a ^ b
a, b:t
Ha:0 < a
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => 0 < a ^ b0)
a, b:t
Ha:0 < a
Hb:0 <= b
0 < a ^ 0
a, b:t
Ha:0 < a
Hb:0 <= b
forall m : t, 0 <= m -> 0 < a ^ m -> 0 < a ^ S m
a, b:t
Ha:0 < a
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => 0 < a ^ b0)
solve_proper.
a, b:t
Ha:0 < a
Hb:0 <= b

0 < a ^ 0
nzsimpl; order'.
a, b:t
Ha:0 < a
Hb:0 <= b

forall m : t, 0 <= m -> 0 < a ^ m -> 0 < a ^ S m
a:t
Ha:0 < a

forall m : t, 0 <= m -> 0 < a ^ m -> 0 < a ^ S m
a:t
Ha:0 < a
b:t
Hb:0 <= b
IH:0 < a ^ b

0 < a ^ S b
a:t
Ha:0 < a
b:t
Hb:0 <= b
IH:0 < a ^ b

0 < a * a ^ b
now apply mul_pos_pos. Qed.
Monotonicity

forall a b c : t, 0 < c -> 0 <= a < b -> a ^ c < b ^ c

forall a b c : t, 0 < c -> 0 <= a < b -> a ^ c < b ^ c
a, b, c:t
Hc:0 < c

0 <= a < b -> a ^ c < b ^ c
a, b, c:t
Hc:0 < c

Proper (eq ==> iff) (fun c0 : t => 0 <= a < b -> a ^ c0 < b ^ c0)
a, b, c:t
Hc:0 < c
0 <= a < b -> a ^ S 0 < b ^ S 0
a, b, c:t
Hc:0 < c
forall m : t, 0 < m -> (0 <= a < b -> a ^ m < b ^ m) -> 0 <= a < b -> a ^ S m < b ^ S m
a, b, c:t
Hc:0 < c

Proper (eq ==> iff) (fun c0 : t => 0 <= a < b -> a ^ c0 < b ^ c0)
solve_proper.
a, b, c:t
Hc:0 < c

0 <= a < b -> a ^ S 0 < b ^ S 0
a, b, c:t
Hc:0 < c
Ha:0 <= a
H:a < b

a ^ S 0 < b ^ S 0
nzsimpl; trivial; order.
a, b, c:t
Hc:0 < c

forall m : t, 0 < m -> (0 <= a < b -> a ^ m < b ^ m) -> 0 <= a < b -> a ^ S m < b ^ S m
a, b:t

forall m : t, 0 < m -> (0 <= a < b -> a ^ m < b ^ m) -> 0 <= a < b -> a ^ S m < b ^ S m
a, b, c:t
Hc:0 < c
IH:0 <= a < b -> a ^ c < b ^ c
Ha:0 <= a
H:a < b

a ^ S c < b ^ S c
a, b, c:t
Hc:0 < c
IH:0 <= a < b -> a ^ c < b ^ c
Ha:0 <= a
H:a < b

a * a ^ c < b * b ^ c
a, b, c:t
Hc:0 < c
IH:0 <= a < b -> a ^ c < b ^ c
Ha:0 <= a
H:a < b

0 <= a ^ c
a, b, c:t
Hc:0 < c
IH:0 <= a < b -> a ^ c < b ^ c
Ha:0 <= a
H:a < b
a ^ c < b ^ c
a, b, c:t
Hc:0 < c
IH:0 <= a < b -> a ^ c < b ^ c
Ha:0 <= a
H:a < b

0 <= a ^ c
apply pow_nonneg; try order.
a, b, c:t
Hc:0 < c
IH:0 <= a < b -> a ^ c < b ^ c
Ha:0 <= a
H:a < b

a ^ c < b ^ c
a, b, c:t
Hc:0 < c
IH:0 <= a < b -> a ^ c < b ^ c
Ha:0 <= a
H:a < b

0 <= a < b
now split. Qed.

forall a b c : t, 0 <= a <= b -> a ^ c <= b ^ c

forall a b c : t, 0 <= a <= b -> a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
H:a <= b

a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:c < 0

a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:c == 0
a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:c < 0

a ^ c <= b ^ c
rewrite !(pow_neg_r _ _ Hc); now nzsimpl.
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:c == 0

a ^ c <= b ^ c
rewrite Hc; now nzsimpl.
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c

a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
H:a < b \/ a == b
Hc:0 < c

a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
H:a < b
Hc:0 < c

a ^ c <= b ^ c
apply lt_le_incl, pow_lt_mono_l; now try split. Qed.

forall a b : t, 1 < a -> 0 < b <-> 1 < a ^ b

forall a b : t, 1 < a -> 0 < b <-> 1 < a ^ b
a, b:t
Ha:1 < a

0 < b <-> 1 < a ^ b
a, b:t
Ha:1 < a
Hb:0 < b

1 < a ^ b
a, b:t
Ha:1 < a
Hb:1 < a ^ b
0 < b
a, b:t
Ha:1 < a
Hb:0 < b

1 < a ^ b
a, b:t
Ha:1 < a
Hb:0 < b

1 ^ b < a ^ b
apply pow_lt_mono_l; try split; order'.
a, b:t
Ha:1 < a
Hb:1 < a ^ b

0 < b
a, b:t
Ha:1 < a
Hb:1 < a ^ b
H:b < 0

0 < b
a, b:t
Ha:1 < a
Hb:1 < a ^ b
H:b == 0
0 < b
a, b:t
Ha:1 < a
Hb:1 < a ^ b
H:b < 0

0 < b
rewrite pow_neg_r in Hb; order'.
a, b:t
Ha:1 < a
Hb:1 < a ^ b
H:b == 0

0 < b
a, b:t
Ha:1 < a
Hb:1 < 1
H:b == 0

0 < b
order. Qed.

forall a b c : t, 1 < a -> 0 <= c -> b < c -> a ^ b < a ^ c

forall a b c : t, 1 < a -> 0 <= c -> b < c -> a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c

a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:b < 0

a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:b < 0

a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:b < 0

0 < a ^ c
apply pow_pos_nonneg; order'.
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b

a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c

a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
Hd:0 <= d

a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
Hd:0 <= d

a ^ b < a ^ d * a ^ b
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
Hd:0 <= d

1 * a ^ b < a ^ d * a ^ b
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
Hd:0 <= d

0 < a ^ b
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
Hd:0 <= d
1 < a ^ d
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
Hd:0 <= d

0 < a ^ b
apply pow_pos_nonneg; order'.
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
Hd:0 <= d

1 < a ^ d
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
Hd:0 <= d

0 < d
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == d + b
EQ':0 == d

0 < d
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == 0 + b
EQ':0 == d

0 < 0
a, b, c:t
Ha:1 < a
Hc:0 <= c
H:b < c
Hb:0 <= b
H':b <= c
d:t
EQ:c == b
EQ':0 == d

0 < 0
order. Qed.
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 ^ c

forall a b c : t, 0 < a -> b <= c -> a ^ b <= a ^ c
a, b, c:t
Ha:0 < a
H:b <= c

a ^ b <= a ^ c
a, b, c:t
Ha:0 < a
H:b <= c
Hb:b < 0

a ^ b <= a ^ c
a, b, c:t
Ha:0 < a
H:b <= c
Hb:0 <= b
a ^ b <= a ^ c
a, b, c:t
Ha:0 < a
H:b <= c
Hb:b < 0

a ^ b <= a ^ c
a, b, c:t
Ha:0 < a
H:b <= c
Hb:b < 0

0 <= a ^ c
apply pow_nonneg; order.
a, b, c:t
Ha:0 < a
H:b <= c
Hb:0 <= b

a ^ b <= a ^ c
a, b, c:t
Ha:1 <= a
H:b <= c
Hb:0 <= b

a ^ b <= a ^ c
a, b, c:t
Ha:1 < a
H:b <= c
Hb:0 <= b

a ^ b <= a ^ c
a, b, c:t
Ha:1 == a
H:b <= c
Hb:0 <= b
1 ^ b <= 1 ^ c
a, b, c:t
Ha:1 < a
H:b <= c
Hb:0 <= b

a ^ b <= a ^ c
a, b, c:t
Ha:1 < a
H:b < c
Hb:0 <= b

a ^ b <= a ^ c
apply lt_le_incl, pow_lt_mono_r; order.
a, b, c:t
Ha:1 == a
H:b <= c
Hb:0 <= b

1 ^ b <= 1 ^ c
nzsimpl; order. Qed.

forall a b c d : t, 0 < a <= c -> b <= d -> a ^ b <= c ^ d

forall a b c d : t, 0 < a <= c -> b <= d -> a ^ b <= c ^ d
a, b, c, d:t
H:0 < a <= c
H0:b <= d

a ^ b <= c ^ d
a, b, c, d:t
H:0 < a <= c
H0:b <= d

a ^ b <= a ^ d
a, b, c, d:t
H:0 < a <= c
H0:b <= d
a ^ d <= c ^ d
a, b, c, d:t
H:0 < a <= c
H0:b <= d

a ^ b <= a ^ d
apply pow_le_mono_r; intuition order.
a, b, c, d:t
H:0 < a <= c
H0:b <= d

a ^ d <= c ^ d
apply pow_le_mono_l; intuition order. Qed.

forall a b c d : t, 0 < a < c -> 0 < b < d -> a ^ b < c ^ d

forall a b c d : t, 0 < a < c -> 0 < b < d -> a ^ b < c ^ d
a, b, c, d:t
Ha:0 < a
Hac:a < c
Hb:0 < b
Hbd:b < d

a ^ b < c ^ d
a, b, c, d:t
Ha:1 <= a
Hac:a < c
Hb:0 < b
Hbd:b < d

a ^ b < c ^ d
a, b, c, d:t
Ha:1 < a
Hac:a < c
Hb:0 < b
Hbd:b < d

a ^ b < c ^ d
a, b, c, d:t
Ha:1 == a
Hac:a < c
Hb:0 < b
Hbd:b < d
1 ^ b < c ^ d
a, b, c, d:t
Ha:1 < a
Hac:a < c
Hb:0 < b
Hbd:b < d

a ^ b < c ^ d
a, b, c, d:t
Ha:1 < a
Hac:a < c
Hb:0 < b
Hbd:b < d

a ^ b < a ^ d
a, b, c, d:t
Ha:1 < a
Hac:a < c
Hb:0 < b
Hbd:b < d
a ^ d < c ^ d
a, b, c, d:t
Ha:1 < a
Hac:a < c
Hb:0 < b
Hbd:b < d

a ^ b < a ^ d
apply pow_lt_mono_r; intuition order.
a, b, c, d:t
Ha:1 < a
Hac:a < c
Hb:0 < b
Hbd:b < d

a ^ d < c ^ d
apply pow_lt_mono_l; try split; order'.
a, b, c, d:t
Ha:1 == a
Hac:a < c
Hb:0 < b
Hbd:b < d

1 ^ b < c ^ d
a, b, c, d:t
Ha:1 == a
Hac:a < c
Hb:0 < b
Hbd:b < d

1 < c ^ d
apply pow_gt_1; order. Qed.
Injectivity

forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a ^ c == b ^ c -> a == b

forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a ^ c == b ^ c -> a == b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
EQ:a ^ c == b ^ c

a == b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
EQ:a ^ c == b ^ c
LT:a < b

a == b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
EQ:a ^ c == b ^ c
GT:b < a
a == b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
EQ:a ^ c == b ^ c
LT:a < b

a == b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
EQ:a ^ c == b ^ c
LT:a < b
H:a ^ c < b ^ c

a == b
order.
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
EQ:a ^ c == b ^ c
GT:b < a

a == b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
EQ:a ^ c == b ^ c
GT:b < a
H:b ^ c < a ^ c

a == b
order. Qed.

forall a b c : t, 1 < a -> 0 <= b -> 0 <= c -> a ^ b == a ^ c -> b == c

forall a b c : t, 1 < a -> 0 <= b -> 0 <= c -> a ^ b == a ^ c -> b == c
a, b, c:t
Ha:1 < a
Hb:0 <= b
Hc:0 <= c
EQ:a ^ b == a ^ c

b == c
a, b, c:t
Ha:1 < a
Hb:0 <= b
Hc:0 <= c
EQ:a ^ b == a ^ c
LT:b < c

b == c
a, b, c:t
Ha:1 < a
Hb:0 <= b
Hc:0 <= c
EQ:a ^ b == a ^ c
GT:c < b
b == c
a, b, c:t
Ha:1 < a
Hb:0 <= b
Hc:0 <= c
EQ:a ^ b == a ^ c
LT:b < c

b == c
a, b, c:t
Ha:1 < a
Hb:0 <= b
Hc:0 <= c
EQ:a ^ b == a ^ c
LT:b < c
H:a ^ b < a ^ c

b == c
order.
a, b, c:t
Ha:1 < a
Hb:0 <= b
Hc:0 <= c
EQ:a ^ b == a ^ c
GT:c < b

b == c
a, b, c:t
Ha:1 < a
Hb:0 <= b
Hc:0 <= c
EQ:a ^ b == a ^ c
GT:c < b
H:a ^ c < a ^ b

b == c
order. Qed.
Monotonicity results, both ways

forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a < b <-> a ^ c < b ^ c

forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a < b <-> a ^ c < b ^ c
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

a < b <-> a ^ c < b ^ c
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LT:a < b

a ^ c < b ^ c
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LT:a ^ c < b ^ c
a < b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LT:a < b

a ^ c < b ^ c
apply pow_lt_mono_l; try split; trivial.
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LT:a ^ c < b ^ c

a < b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LT:a ^ c < b ^ c
LE:b <= a

a < b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LT:a ^ c < b ^ c
LE:b <= a
H:b ^ c <= a ^ c

a < b
order. Qed.

forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a <= b <-> a ^ c <= b ^ c

forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a <= b <-> a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

a <= b <-> a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LE:a <= b

a ^ c <= b ^ c
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LE:a ^ c <= b ^ c
a <= b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LE:a <= b

a ^ c <= b ^ c
apply pow_le_mono_l; try split; trivial.
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LE:a ^ c <= b ^ c

a <= b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LE:a ^ c <= b ^ c
GT:b < a

a <= b
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
LE:a ^ c <= b ^ c
GT:b < a
H:b ^ c < a ^ c

a <= b
order. Qed.

forall a b c : t, 1 < a -> 0 <= c -> b < c <-> a ^ b < a ^ c

forall a b c : t, 1 < a -> 0 <= c -> b < c <-> a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c

b < c <-> a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LT:b < c

a ^ b < a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LT:a ^ b < a ^ c
b < c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LT:b < c

a ^ b < a ^ c
now apply pow_lt_mono_r.
a, b, c:t
Ha:1 < a
Hc:0 <= c
LT:a ^ b < a ^ c

b < c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LT:a ^ b < a ^ c
LE:c <= b

b < c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LT:a ^ b < a ^ c
LE:c <= b
H:a ^ c <= a ^ b

b < c
order. Qed.

forall a b c : t, 1 < a -> 0 <= c -> b <= c <-> a ^ b <= a ^ c

forall a b c : t, 1 < a -> 0 <= c -> b <= c <-> a ^ b <= a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c

b <= c <-> a ^ b <= a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LE:b <= c

a ^ b <= a ^ c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LE:a ^ b <= a ^ c
b <= c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LE:b <= c

a ^ b <= a ^ c
apply pow_le_mono_r; order'.
a, b, c:t
Ha:1 < a
Hc:0 <= c
LE:a ^ b <= a ^ c

b <= c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LE:a ^ b <= a ^ c
GT:c < b

b <= c
a, b, c:t
Ha:1 < a
Hc:0 <= c
LE:a ^ b <= a ^ c
GT:c < b
H:a ^ c < a ^ b

b <= c
order. Qed.
For any a>1, the a^x function is above the identity function

forall a b : t, 1 < a -> 0 <= b -> b < a ^ b

forall a b : t, 1 < a -> 0 <= b -> b < a ^ b
a, b:t
Ha:1 < a
Hb:0 <= b

b < a ^ b
a, b:t
Ha:1 < a
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => b0 < a ^ b0)
a, b:t
Ha:1 < a
Hb:0 <= b
0 < a ^ 0
a, b:t
Ha:1 < a
Hb:0 <= b
forall m : t, 0 <= m -> m < a ^ m -> S m < a ^ S m
a, b:t
Ha:1 < a
Hb:0 <= b

Proper (eq ==> iff) (fun b0 : t => b0 < a ^ b0)
solve_proper.
a, b:t
Ha:1 < a
Hb:0 <= b

0 < a ^ 0
a, b:t
Ha:1 < a
Hb:0 <= b

0 < 1
order'.
a, b:t
Ha:1 < a
Hb:0 <= b

forall m : t, 0 <= m -> m < a ^ m -> S m < a ^ S m
a:t
Ha:1 < a

forall m : t, 0 <= m -> m < a ^ m -> S m < a ^ S m
a:t
Ha:1 < a
b:t
Hb:0 <= b
IH:b < a ^ b

S b < a ^ S b
a:t
Ha:1 < a
b:t
Hb:0 <= b
IH:b < a ^ b

S b < a * a ^ b
a:t
Ha:S 1 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

S (S b) <= a * a ^ b
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

S (S b) <= a * a ^ b
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

S (S b) <= 2 * S b
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b
2 * S b <= a * a ^ b
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

S (S b) <= 2 * S b
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

S (S b) <= S (S (b + b))
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

b <= b + b
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

0 + b <= b + b
apply add_le_mono; order.
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

2 * S b <= a * a ^ b
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

0 <= 2
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b
0 <= S b
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

0 <= 2
order'.
a:t
Ha:2 <= a
b:t
Hb:0 <= b
IH:S b <= a ^ b

0 <= S b
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.

forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a ^ c + b ^ c <= (a + b) ^ c

forall a b c : t, 0 <= a -> 0 <= b -> 0 < c -> a ^ c + b ^ c <= (a + b) ^ c
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

a ^ c + b ^ c <= (a + b) ^ c
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

Proper (eq ==> iff) (fun c0 : t => a ^ c0 + b ^ c0 <= (a + b) ^ c0)
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
a ^ S 0 + b ^ S 0 <= (a + b) ^ S 0
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
forall m : t, 0 < m -> a ^ m + b ^ m <= (a + b) ^ m -> a ^ S m + b ^ S m <= (a + b) ^ S m
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

Proper (eq ==> iff) (fun c0 : t => a ^ c0 + b ^ c0 <= (a + b) ^ c0)
solve_proper.
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

a ^ S 0 + b ^ S 0 <= (a + b) ^ S 0
nzsimpl; order.
a, b, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

forall m : t, 0 < m -> a ^ m + b ^ m <= (a + b) ^ m -> a ^ S m + b ^ S m <= (a + b) ^ S m
a, b:t
Ha:0 <= a
Hb:0 <= b

forall m : t, 0 < m -> a ^ m + b ^ m <= (a + b) ^ m -> a ^ S m + b ^ S m <= (a + b) ^ S m
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c

a ^ S c + b ^ S c <= (a + b) ^ S c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

a ^ S c + b ^ S c <= (a + b) ^ S c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

a * a ^ c + b * b ^ c <= (a + b) * (a + b) ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

a * a ^ c + b * b ^ c <= (a + b) * (a ^ c + b ^ c)
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c
(a + b) * (a ^ c + b ^ c) <= (a + b) * (a + b) ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

a * a ^ c + b * b ^ c <= (a + b) * (a ^ c + b ^ c)
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

a * a ^ c + b * b ^ c <= a * a ^ c + a * b ^ c + (b * a ^ c + b * b ^ c)
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

a * a ^ c <= a * a ^ c + a * b ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c
b * b ^ c <= b * a ^ c + b * b ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

a * a ^ c <= a * a ^ c + a * b ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

a * a ^ c + 0 <= a * a ^ c + a * b ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

0 <= a * b ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

0 <= b ^ c
apply pow_nonneg; trivial.
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

b * b ^ c <= b * a ^ c + b * b ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

0 + b * b ^ c <= b * a ^ c + b * b ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

0 <= b * a ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

0 <= a ^ c
apply pow_nonneg; trivial.
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

(a + b) * (a ^ c + b ^ c) <= (a + b) * (a + b) ^ c
a, b:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:a ^ c + b ^ c <= (a + b) ^ c
H:0 <= c

0 <= a + b
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

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)

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)
(* begin *)

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:t
Ha:0 <= a
H:a <= b
Hc:0 < c

(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c

a * a ^ c + b * a ^ c + (a * b ^ c + b * b ^ c) <= 2 * (a * a ^ c) + 2 * (b * b ^ c)
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c

a * 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:t
Ha:0 <= a
H:a <= b
Hc:0 < c

a * 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:t
Ha:0 <= a
H:a <= b
Hc:0 < c

b * a ^ c + (a * b ^ c + b * b ^ c) <= a * a ^ c + (b * b ^ c + b * b ^ c)
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c

b * a ^ c + a * b ^ c + b * b ^ c <= a * a ^ c + b * b ^ c + b * b ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c

b * a ^ c + a * b ^ c <= a * a ^ c + b * b ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
d:t
EQ:b == d + a
Hd:0 <= d

b * a ^ c + a * b ^ c <= a * a ^ c + b * b ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
d:t
EQ:b == d + a
Hd:0 <= d

(d + a) * a ^ c + a * (d + a) ^ c <= a * a ^ c + (d + a) * (d + a) ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
d:t
EQ:b == d + a
Hd:0 <= d

d * a ^ c + a * a ^ c + a * (d + a) ^ c <= a * a ^ c + (d * (d + a) ^ c + a * (d + a) ^ c)
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
d:t
EQ:b == d + a
Hd:0 <= d

d * a ^ c + a * a ^ c + a * (d + a) ^ c <= a * a ^ c + d * (d + a) ^ c + a * (d + a) ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
d:t
EQ:b == d + a
Hd:0 <= d

d * a ^ c + a * a ^ c <= a * a ^ c + d * (d + a) ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
d:t
EQ:b == d + a
Hd:0 <= d

a * a ^ c + d * a ^ c <= a * a ^ c + d * (d + a) ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
d:t
EQ:b == d + a
Hd:0 <= d

d * a ^ c <= d * (d + a) ^ c
a, b, c:t
Ha:0 <= a
H:a <= b
Hc:0 < c
d:t
EQ:b == d + a
Hd:0 <= d

a ^ c <= (d + a) ^ c
apply pow_le_mono_l; try split; order. (* end *)
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)
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:t
Ha:0 <= a
Hb:0 <= b
Hc: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:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

Proper (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:t
Ha:0 <= a
Hb:0 <= b
Hc: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:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c
forall 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, c:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

Proper (eq ==> iff) (fun c0 : t => (a + b) ^ c0 <= 2 ^ P c0 * (a ^ c0 + b ^ c0))
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:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

(a + b) ^ S 0 <= 2 ^ P (S 0) * (a ^ S 0 + b ^ S 0)
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:t
Ha:0 <= a
Hb:0 <= b
Hc:0 < c

forall 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:t
Ha:0 <= a
Hb:0 <= b

forall 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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c

0 <= a + b
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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c

2 ^ 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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c

2 ^ 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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c

2 ^ 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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2

2 ^ 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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2

2 ^ 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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2

0 <= 2 ^ P 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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2

0 <= 2 ^ P 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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2
H0: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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2
H0:b < a
(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2
H0:a <= b

(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2
H0:b < a

(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:t
Ha:0 <= a
Hb:0 <= b
c:t
Hc:0 < c
IH:(a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
H:0 <= c
EQ:S (P c) == c
LE:0 <= P c
EQ':2 ^ c == 2 ^ P c * 2
H0:b < a

(b + a) * (b ^ c + a ^ c) <= 2 * (b * b ^ c + a * a ^ c)
apply aux; try split; order'. Qed. End NZPowProp.