proposition: Lemma gcd_mul_mono_r_nonneg : forall n m p, 0<=p -> gcd (n*p) (m*p) == gcd n m * p.
proof: Proof. intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd