Theorem: IMOSL.IMO2014A4.linear_good (IMOSLLean4/IMO2014/A4/A4.lean)

State before:
b c : ℤ
h : b - 1 ∣ c
⊢ good b c fun x => (b - 1) * x + c / (b - 1)
Tactic:
nth_rw 1 [← sub_add_cancel b 1, ← Int.mul_ediv_cancel' h]
State after:
b c : ℤ
h : b - 1 ∣ c
⊢ good (b - 1 + 1) ((b - 1) * (c / (b - 1))) fun x => (b - 1) * x + c / (b - 1)

State before:
b c : ℤ
h : b - 1 ∣ c
⊢ good (b - 1 + 1) ((b - 1) * (c / (b - 1))) fun x => (b - 1) * x + c / (b - 1)
Tactic:
exact linear_good' (b - 1) (c / (b - 1))
State after:
no goals