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!