Return to Revisions

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.