proposition: Theorem Gauss : forall a b c:Z, (a | b * c) -> rel_prime a b -> (a | c).
proof: Proof. intros a b c H H0. elim (rel_prime_bezout a b H0); intros u v H1. replace c with (c * 1); [ idtac | ring ]. rewrite <- H1. replace (c * (u * a + v * b)) with (c * u * a + v * (b * c)); [ eauto with zarith | ring ]. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat