proposition: Lemma Zdivides_mult_intro_lft : forall a b c : Z, Zdivides (a * b) c -> Zdivides b c.
proof: Proof. intros a b c H. unfold Zdivides in H; elim H; intros q H_. exists (q * a)%Z. rewrite <- Zmult_assoc. assumption. Qed.
imports: CoRN.model.Zmod.ZBasics