proposition: Theorem first_power_le : ∀ pow cl h hv, (h, hv) ∈ filter_finite_ord (qpower_list pow cl) → pow ≤ Z.to_nat (Qnum h).
proof: Proof. intros pow cl h hv Hhhv. unfold qpower_list in Hhhv. revert pow Hhhv. induction cl as [| c]; intros; [ contradiction | idtac ]. simpl in Hhhv. destruct cl as [| c₁]. simpl in Hhhv. destruct (order c); [ idtac | contradiction ]. destruct Hhhv as [Hhhv| ]; [ idtac | contradiction ]. injection Hhhv; clear Hhhv; intros; subst h hv. simpl. rewrite Nat2Z.id; reflexivity. simpl in Hhhv. simpl in IHcl. destruct (order c). destruct Hhhv as [Hhhv| Hhhv]. injection Hhhv; clear Hhhv; intros; subst h hv. simpl; rewrite Nat2Z.id; reflexivity. apply IHcl in Hhhv. transitivity (S pow); [ apply Nat.le_succ_r | assumption ]. left; reflexivity. apply IHcl in Hhhv. transitivity (S pow); [ apply Nat.le_succ_r | assumption ]. left; reflexivity. 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