β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
i : ℕ
⊢ a ^ i ≤ b ^ i
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
⊢ ∀ (i : ℕ), a ^ i ≤ b ^ i
intro i
no goals
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
i : ℕ
⊢ a ^ i ≤ b ^ i
induction i with
| zero =>  simp
| succ k ih =>
  rw [pow_succ, pow_succ]
  apply mul_le_mul hab
  apply ih
  apply pow_nonneg ha
  apply le_trans ha hab
no goals
case zero
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
⊢ a ^ Nat.zero ≤ b ^ Nat.zero
simp
case succ
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a * a ^ k ≤ b * b ^ k
case succ
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a ^ Nat.succ k ≤ b ^ Nat.succ k
rw [pow_succ, pow_succ]
case succ.h₂
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a ^ k ≤ b ^ k

case succ.c0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ a ^ k

case succ.b0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
case succ
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a * a ^ k ≤ b * b ^ k
apply mul_le_mul hab
case succ.c0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ a ^ k

case succ.b0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
case succ.h₂
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ a ^ k ≤ b ^ k

case succ.c0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ a ^ k

case succ.b0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
apply ih
case succ.b0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
case succ.c0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ a ^ k

case succ.b0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
apply pow_nonneg ha
no goals
case succ.b0
β : Type ?u.222009
A : Type ?u.222012
G : Type ?u.222015
M : Type ?u.222018
R : Type u_1
inst✝ : OrderedSemiring R
a✝ x y : R
n m : ℕ
a b : R
ha : 0 ≤ a
hab : a ≤ b
k : ℕ
ih : a ^ k ≤ b ^ k
⊢ 0 ≤ b
apply le_trans ha hab