n a : ℕ
h : a ≤ n + n
⊢ n * n + a < succ (n * n + (n + n))
n a : ℕ
h : a ≤ n + n
⊢ n * n + a < succ n * succ n
rw [succ_mul, mul_succ, add_succ, add_assoc]
no goals
n a : ℕ
h : a ≤ n + n
⊢ n * n + a < succ (n * n + (n + n))
exact lt_succ_of_le (Nat.add_le_add_left h _)