proposition: Lemma Zdivides_mult_cancel_lft : forall a b c : Z, Zdivides a b -> Zdivides (c * a) (c * b).
proof: Proof. intros. unfold Zdivides in H; elim H; intros. exists x. rewrite <- H0. rewrite Zmult_assoc. rewrite Zmult_assoc. rewrite (Zmult_comm x c). reflexivity. Qed.
imports: CoRN.model.Zmod.ZBasics