# How to prove basic lemmas about divisibility in Coq?

Require Import ZArith.

Open Scope Z_scope.

Lemma mod_mult_or : forall a b c, (a | b) \/ (a | c) -> (a | b * c).
Proof.
intros.
destruct H as [H1|H2].
apply Zdivide_mult_l; assumption.
apply Zdivide_mult_r; assumption.
Qed.

Lemma mod_mult : forall a b c, (a | b) /\ (a | c) -> (a | b * c).
Proof.
intros a b c [Hab Hac].
apply Z_divide_mul.
apply Hab.
apply Hac.
Qed.

Close Scope Z_scope.



I keep getting all sorts of errors on both proofs. I am not quite sure how to solve each proof the correct way. If someone can help me thanks!

• Have you tried importing Coq.ZArith.Znumtheory.?
– Couchy
Apr 25 at 3:45
• I am trying to approach it strictly with the ZArith library and using Z_scope. Apr 25 at 16:32

You have to make the quotient explicit in a relation a | b (defined through an existential quantifier).

Lemma mod_mult_or : forall a b c, (a | b) \/ (a | c) -> (a | b * c).
Proof.
intros.
destruct H as [[q1 H1] | [q2 H2]].
- exists (q1 * c).
subst.  repeat rewrite <- Z.mul_assoc.
f_equal; now rewrite (Z.mul_comm  a c).
-

Qed.


• Lemma mod_mult_or : forall a b c, (a | b) \/ (a | c) -> (a | b * c). Proof. intros a b c H. destruct H as [Hb | Hc]. - apply Z.divide_mul_r. exact Hb. - apply Z.divide_mul_l. exact Hc. Qed.  I tried this way but it seems to have not worked. :( Apr 25 at 16:30
• I edited the first sub-goal of the proof. What was the issue with it? Apr 25 at 20:10
• I figured it out. Apr 25 at 21:15
• Just used unfold rewrite exists -> tactic, thanks! Apr 25 at 21:17

Which version of Coq are you using? This should work:

Require Import ZArith.

Open Scope Z_scope.

Lemma mod_mult_or : forall a b c, (a | b) \/ (a | c) -> (a | b * c).
Proof.
intros.
destruct H as [H1|H2].
Search (_ | _ * _).
apply Z.divide_mul_l; assumption.
apply Z.divide_mul_r; assumption.
Qed.

Lemma mod_mult : forall a b c, (a | b) /\ (a | c) -> (a | b * c).
Proof.
intros a b c [Hab Hac].
apply mod_mult_or.
left.
apply Hab.
Qed.

Close Scope Z_scope.