proposition: Theorem Zgcd_div_pos a b: 0 < b -> 0 < Z.gcd a b -> 0 < b / Z.gcd a b.
proof: Proof. intros Hb Hg. assert (H : 0 <= b / Z.gcd a b) by (apply Z.div_pos; auto with zarith). Z.le_elim H; trivial. rewrite (Zdivide_Zdiv_eq (Z.gcd a b) b), <- H, Z.mul_0_r in Hb; auto using Z.gcd_divide_r with zarith. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia