proposition: Theorem in_power_list_lt : ∀ A la h (hv : puiseux_series A) pow, (h, hv) ∈ qpower_list pow la → (nat_num h < pow + length la)%nat.
proof: Proof. intros A la h hv pow Hh. unfold qpower_list in Hh. unfold pair_rec in Hh; simpl in Hh. revert pow Hh. induction la as [| a]; intros; [ contradiction | simpl ]. simpl in Hh. destruct Hh as [Hh| Hh]. injection Hh; clear Hh; intros; subst h hv. rewrite nat_num_Qnat. apply Nat.lt_sub_lt_add_l. rewrite Nat.sub_diag. apply Nat.lt_0_succ. rewrite Nat.add_succ_r, <- Nat.add_succ_l. apply IHla; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m