proposition: Theorem list_seq_app : ∀ j dj len, (dj ≤ len)%nat → List.seq j len = List.seq j dj ++ List.seq (j + dj) (len - dj).
proof: Proof. intros j dj len Hjlen. revert j dj Hjlen. induction len; intros. simpl. apply Nat.le_0_r in Hjlen; subst dj; reflexivity. destruct dj; simpl. rewrite Nat.add_0_r. reflexivity. f_equal. rewrite Nat.add_succ_r, <- Nat.add_succ_l. apply le_S_n in Hjlen. erewrite IHlen; [ reflexivity | eassumption ]. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn