rw [this, Nat.mul_div_right]
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ (4 * (n - 1) + 1 + 3) / 2 = 2 * (n - 1) + 1 + 1
case H
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ 0 < 2