proposition: Theorem p_and_q_have_no_common_factors : ∀ a m p q, p = p_of_m m a → q = q_of_m m a → Z.gcd p (Zpos q) = 1%Z.
proof: Proof. intros a m p q Hp Hq. eapply any_is_p_mq; eauto . Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base