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