Theorem: Nat.pow_lt_pow_right (Algdata/Init/Nat.lean)

State before:
n i j : Nat
⊢ n ≥ 2 → i < j → n ^ i < n ^ j
Tactic:
intro hn hij
State after:
n i j : Nat
hn : n ≥ 2
hij : i < j
⊢ n ^ i < n ^ j

State before:
n i j : Nat
hn : n ≥ 2
hij : i < j
⊢ n ^ i < n ^ j
Tactic:
induction hij
State after:
case refl
n i j : Nat
hn : n ≥ 2
⊢ n ^ i < n ^ succ i

case step
n i j : Nat
hn : n ≥ 2
m✝ : Nat
a✝ : Nat.le (succ i) m✝
a_ih✝ : n ^ i < n ^ m✝
⊢ n ^ i < n ^ succ m✝

State before:
n i j : Nat
hn : n ≥ 2
⊢ n ^ i < n ^ succ i
Tactic:
case refl => calc
  n^i < n^i + n^i := Nat.lt_add_of_pos_left (Nat.pos_pow_of_pos i (trans (Nat.zero_lt_succ 1) hn))
  _   = n^i*2 := (Nat.mul_two _).symm
  _   ≤ n^i*n := Nat.mul_le_mul_left (n^i) hn
State after:
no goals

State before:
n i j✝ : Nat
hn : n ≥ 2
j : Nat
a✝ : Nat.le (succ i) j
h_ind : n ^ i < n ^ j
⊢ n ^ i < n ^ succ j
Tactic:
case step j _ h_ind => calc
  n^i < n^j := h_ind
  _   ≤ n^j + n^j := Nat.le_add_left _ _
  _   = n^j*2 := (Nat.mul_two _).symm
  _   ≤ n^j*n := Nat.mul_le_mul_left _ hn
State after:
no goals

State before:
n i j : Nat
hn : n ≥ 2
⊢ n ^ i < n ^ succ i
Tactic:
calc
n^i < n^i + n^i := Nat.lt_add_of_pos_left (Nat.pos_pow_of_pos i (trans (Nat.zero_lt_succ 1) hn))
_   = n^i*2 := (Nat.mul_two _).symm
_   ≤ n^i*n := Nat.mul_le_mul_left (n^i) hn
State after:
no goals

State before:
n i j✝ : Nat
hn : n ≥ 2
j : Nat
a✝ : Nat.le (succ i) j
h_ind : n ^ i < n ^ j
⊢ n ^ i < n ^ succ j
Tactic:
calc
n^i < n^j := h_ind
_   ≤ n^j + n^j := Nat.le_add_left _ _
_   = n^j*2 := (Nat.mul_two _).symm
_   ≤ n^j*n := Nat.mul_le_mul_left _ hn
State after:
no goals