proposition: Theorem Zgcd_div_swap0 : forall a b : Z, 0 < Z.gcd a b -> 0 < b -> (a / Z.gcd a b) * b = a * (b/Z.gcd a b).
proof: Proof. intros a b Hg Hb. assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3]. pattern b at 2; rewrite (Zdivide_Zdiv_eq (Z.gcd a b) b); auto. repeat rewrite Z.mul_assoc; f_equal. rewrite Z.mul_comm. rewrite <- Zdivide_Zdiv_eq; auto. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat