n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2

case H
n : ℕ
⊢ 0 < 2
n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n
rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, add_tsub_cancel_right, mul_comm]
case H
n : ℕ
⊢ 0 < 2
n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2

case H
n : ℕ
⊢ 0 < 2
cases n <;> rfl
no goals
case H
n : ℕ
⊢ 0 < 2
apply zero_lt_succ