proposition: Theorem length_char_pol_succ : ∀ j x l, (j < power (List.hd x l))%nat → Sorted (λ a b, (power a < power b)%nat) (l ++ [x]) → List.length (make_char_pol R (S j) (l ++ [x])) = (power x - j)%nat.
proof: Proof. intros j x l Hjpx Hsort. revert j x Hjpx Hsort. induction l as [| a]; intros; simpl. rewrite list_length_pad; simpl. simpl in Hjpx. rewrite <- Nat.add_sub_swap; auto with Arith. rewrite Nat.add_1_r; reflexivity. rewrite list_length_pad; simpl. simpl in Hjpx. rewrite IHl. eapply Sorted_trans_app in Hsort; [ idtac | idtac | left; eauto ]. rewrite <- Nat.add_sub_swap; auto with Arith. rewrite <- Nat.sub_succ_l; [ idtac | apply Nat.lt_le_incl; auto ]. rewrite Nat.add_sub_assoc; [ idtac | apply Nat.lt_le_incl; auto ]. rewrite Nat.add_sub_swap; auto with Arith. rewrite Nat.sub_diag; reflexivity. clear x Hsort. intros x y z H₁ H₂; eapply Nat.lt_trans; eassumption. simpl in Hsort. destruct l as [| b]; simpl in Hsort; simpl. apply Sorted_inv_2 in Hsort. destruct Hsort; assumption. apply Sorted_inv_2 in Hsort. destruct Hsort; assumption. simpl in Hsort. apply Sorted_inv in Hsort. destruct Hsort; 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