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.

```