proposition: Remark mult_minus_distr_l : forall a b c : nat, a * (b - c) = a * b - a * c.
proof: Proof. intros a b c; repeat rewrite (Nat.mul_comm a); apply Nat.mul_sub_distr_r. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)