proposition: Theorem num_m_den_is_pos : ∀ f L j αj m, newton_segments f = Some L → pol_in_K_1_m f m → ini_pt L = (Qnat j, αj) → (0 < Qnum αj)%Z → (0 < Z.to_nat (Qnum αj * Zpos m / Zpos (Qden αj)))%nat.
proof: Proof. intros f L j αj m HL Hm Hini Hn. assert (Zpos (Qden αj) | Qnum αj * Zpos m)%Z as H. eapply den_αj_divides_num_αj_m; eassumption. destruct H as (d, Hd). rewrite Hd. rewrite Z.div_mul; [ | apply Pos2Z_ne_0 ]. destruct d as [| d| d]. simpl in Hd. apply Z.eq_mul_0_l in Hd; [ | apply Pos2Z_ne_0 ]. rewrite Hd in Hn. exfalso; revert Hn; apply Z.lt_irrefl. apply Pos2Nat.is_pos. simpl in Hd. pose proof (Pos2Z.neg_is_neg (d * Qden αj)) as I. rewrite <- Hd in I. apply Z.nle_gt in I. exfalso; apply I. apply Z.mul_nonneg_nonneg; [ | apply Pos2Z.is_nonneg]. apply Z.lt_le_incl; assumption. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM