proposition: Theorem p_is_pos : ∀ L αj αk m r, ini_pt L = (Qnat 0, αj) → fin_pt L = (Qnat r, αk) → (0 < Qnum αj)%Z → Qnum αk = 0%Z → (0 < r)%nat → (0 < p_of_m m (γ L))%Z.
proof: Proof. intros L αj αk m r Hini Hfin Hαj Hαk Hr. unfold p_of_m; simpl. rewrite Hini, Hfin; simpl. rewrite Hαk; simpl. rewrite Qnum_inv_Qnat_sub; [ | assumption ]. rewrite Qden_inv_Qnat_sub; [ | assumption ]. rewrite Z.add_0_r, Z.mul_1_r, Nat.sub_0_r. rewrite Z.gcd_comm. apply Z_div_gcd_r_pos. apply Z.mul_pos_pos; [ | apply Pos2Z.is_pos ]. apply Z.mul_pos_pos; [ assumption | apply Pos2Z.is_pos ]. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail