calc
m^i.succ = m^i * m := rfl
_        ≤ n^i * m := Nat.mul_le_mul_right m (Nat.pow_le_pow_of_le_left (Nat.le_of_lt hmn) i)
_        < n^i * n := Nat.mul_lt_mul_of_pos_left hmn (Nat.pos_pow_of_pos i (trans m.zero_le hmn))
m n : Nat
hmn : m < n
i : Nat
hi : succ i > 0
⊢ m ^ succ i < n ^ succ i
no goals