proposition: Lemma gcd_quot_factor : forall a b c, 0<c -> (c|a) -> (c|b) -> gcd (a÷c) (b÷c) == (gcd a b)÷c.
proof: Proof. intros a b c Hc Ha Hb. rewrite !quot_div_exact; trivial; try order. - now apply gcd_div_factor. - now apply gcd_greatest. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor