You have to make the quotient explicit in a relation `a | b` (defined through an existential quantifier). ``` 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 [[q1 H1] | [q2 H2]]. - exists (q1 * c). (* I let you complete the proofs ... *) ```