n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n
n : ℕ
h : 1 < n
⊢ n < n * n
have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h)
no goals
n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n
rwa [mul_one] at this