Theorem: IMOSL.Extra.IntIntLinearSolverAlt (IMOSLLean4/Extra/IntLinearSolver.lean)

State before:
g : ℤ
f : ℤ → ℤ
h : ∀ (n : ℤ), f (n + 1) = g + f n
n : ℤ
⊢ f n = g * n + f 0
Tactic:
rw [IntLinearSolver h, smul_eq_mul, mul_comm]
State after:
no goals