ring_nf
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ 3 * (j * j + j) + (j + j + (j + j + 1) / 2) + (j + j + (j + j + 2) / 2) = Nat.succ (3 * ((j + 1) * j + j + j))
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ j * 7 + j ^ 2 * 3 + (1 + j * 2) / 2 + (2 + j * 2) / 2 = Nat.succ (j * 9 + j ^ 2 * 3)