proposition: Theorem List_seq_split_last : ∀ len start, List.seq start (S len) = List.seq start len ++ [start + len]%nat.
proof: Proof. intros len start; simpl. revert start. induction len; intros; simpl. rewrite Nat.add_0_r; reflexivity. rewrite Nat.add_succ_r, <- Nat.add_succ_l. rewrite <- IHlen; reflexivity. 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