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