Return to Revisions

You have to explicit the quotient 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 ... *)