proposition: Theorem list_length_pad : ∀ n (z : α) l, List.length (list_pad n z l) = (n + List.length l)%nat.
proof: Proof. intros n z l. induction n; [ reflexivity | simpl ]. rewrite IHn; 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