proposition: Lemma Zmult_divide_compat_rev_l: forall a b c : Z, c <> 0 -> (c * a | c * b) -> (a | b).
proof: Proof. intros a b c Nc (k, Hk). exists k. eapply Zmult_reg_l; eauto. rewrite Hk; ring. Qed.
imports: ZArith Lia Znumtheory