proposition: Theorem any_is_p_mq : ∀ a m p q, p = p_of_m m a → q = q_of_m m a → a == p # (m * q) ∧ Z.gcd p (Zpos q) = 1%Z.
proof: Proof. intros a m p q Hp Hq. unfold Qeq; simpl. subst p q; simpl. unfold p_of_m, q_of_m; simpl. remember (Qnum a * Zpos m)%Z as p. remember (Qden a) as q. remember (Z.gcd p (Zpos q)) as g. rewrite Pos2Z.inj_mul. rewrite Z.mul_assoc. rewrite <- Heqp. pose proof (Z.gcd_divide_l p (Zpos q)). rewrite <- Heqg in H. destruct H as (gp, Hgp). rewrite Hgp. assert (g ≠ 0)%Z as Hg0. intros H. rewrite Heqg in H. apply Z.gcd_eq_0_r in H; revert H; apply Pos2Z_ne_0. rewrite Z.div_mul; auto. pose proof (Z.gcd_divide_r p (Zpos q)). rewrite <- Heqg in H. destruct H as (gq, Hgq). rewrite Hgq. rewrite Z.div_mul; auto. rewrite Z.mul_shuffle0, Z.mul_assoc. rewrite Z2Pos.id. split; [ reflexivity | idtac ]. apply Z.gcd_div_gcd in Heqg; auto. rewrite Hgp, Hgq in Heqg. rewrite Z.div_mul in Heqg; auto. rewrite Z.div_mul in Heqg; auto. apply Z.mul_lt_mono_pos_r with (p := g). symmetry in Heqg. destruct g as [| g| g]. rewrite Z.mul_0_r in Hgq. exfalso; revert Hgq; apply Pos2Z_ne_0. apply Pos2Z.is_pos. pose proof (Z.gcd_nonneg p (Zpos q)). rewrite Heqg in H. apply Z.nlt_ge in H. exfalso; apply H. apply Pos2Z.neg_is_neg. simpl. rewrite <- Hgq; apply Pos2Z.is_pos. 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