proposition: Lemma gcd_div_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. apply mul_cancel_l with c; try order. assert (H:=gcd_greatest _ _ _ Ha Hb). apply mod_divide, div_exact in H; try order. rewrite <- H. rewrite <- gcd_mul_mono_l_nonneg; try order. f_equiv; symmetry; apply div_exact; try order; apply mod_divide; trivial; try order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor