proposition: Lemma gcd_quot_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 !quot_div_exact; trivial. - now apply gcd_div_gcd. - rewrite EQ; apply gcd_divide_r. - rewrite EQ; apply gcd_divide_l. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor