have h1 : (4 * (n - 1) + 1 + 5) = 2 * (2 * (n - 1) + 1 + 2) := by ring
n : ℕ
⊢ (4 * (n - 1) + 1 + 5) / 2 = 2 * (n - 1) + 1 + 2
n : ℕ
h1 : 4 * (n - 1) + 1 + 5 = 2 * (2 * (n - 1) + 1 + 2)
⊢ (4 * (n - 1) + 1 + 5) / 2 = 2 * (n - 1) + 1 + 2