proposition: Lemma gcd_div_gcd : forall a b g, g~=0 -> g == gcd a b -> gcd (a/g) (b/g) == 1.
proof: Proof. intros a b g NZ EQ. rewrite gcd_div_factor. - now rewrite <- EQ, div_same. - generalize (gcd_nonneg a b); order. - rewrite EQ; apply gcd_divide_l. - rewrite EQ; apply gcd_divide_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor