proposition: Lemma div_mult_compat_l : forall a b c : nat, divide a b -> divide a (b * c).
proof: Proof. intros. destruct H. exists (c * x). lia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow