Theorem: IMOSL.IMO2019N4.linear_is_goodPNat (IMOSLLean4/IMO2019/N4/N4.lean)

State before:
C k a b : ℕ+
x✝ : C < a + b
⊢ a ^ 2 + b * (fun x => k * x) a = (a + (fun x => k * x) b) * a
Tactic:
rw [sq, add_mul, mul_assoc, mul_left_comm]
State after:
no goals