proposition: Theorem Zdivide_mult_rel_prime: forall a b c : Z, (a | c) -> (b | c) -> rel_prime a b -> (a * b | c).
proof: Proof. intros a b c (q1, H1) (q2, H2) H3. assert (H4: (a | q2)). apply Gauss with (2 := H3). exists q1; rewrite <- H1; rewrite H2; auto with zarith. case H4; intros q3 H5; exists q3; rewrite H2; rewrite H5; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange