proposition: Theorem pmq_qmpm : ∀ m p q j k jz kz mj mk, (j < k)%nat → jz = Z.of_nat j → kz = Z.of_nat k → p # m * q == (mj - mk # m) / (kz - jz # 1) → Zpos q * (mj - mk) = p * (kz - jz).
proof: Proof. intros m p q j k jz kz mj mk Hjk Hjz Hkz Hpq. subst jz kz. unfold Qeq in Hpq; simpl in Hpq. do 2 rewrite Pos2Z.inj_mul in Hpq. rewrite Zmult_comm in Hpq; symmetry in Hpq. rewrite Zmult_comm in Hpq; symmetry in Hpq. do 2 rewrite <- Zmult_assoc in Hpq. apply Z.mul_cancel_l in Hpq; [ idtac | apply Pos2Z_ne_0 ]. rewrite Zmult_assoc, Zmult_comm in Hpq. rewrite Qden_inv in Hpq. rewrite Qnum_inv in Hpq. symmetry in Hpq. rewrite Zmult_comm in Hpq. symmetry in Hpq. apply Z.div_unique_exact in Hpq; [ idtac | apply Pos2Z_ne_0 ]. rewrite Hpq. rewrite Znumtheory.Zdivide_Zdiv_eq_2. rewrite Z.div_1_r; reflexivity. apply Pos2Z.is_pos. apply Z.divide_1_l. apply Z.lt_0_sub, inj_lt; assumption. apply Z.lt_0_sub, inj_lt; assumption. 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