proposition: Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p).
proof: Proof. intros n m p H G. destruct (gcd_bezout n m 1 G) as (a & b & EQ). rewrite <- (mul_1_l p), <- EQ, mul_add_distr_r. apply divide_add_r. - rewrite mul_shuffle0. apply divide_factor_r. - rewrite <- mul_assoc. now apply divide_mul_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd