proposition: Lemma take_nth_drop : forall (i k : nat) (s : seq K), i <= k -> k < size s -> take (S k) s = take i s ++ (nth Zero s i) :: (take (k - i) (drop (i + 1) s)).
proof: Proof. intro i; induction i. intros k s H H0; destruct s. inversion H0; simpl. replace (k - 0) with k by omega; simpl. rewrite drop0; reflexivity. intros k s H H0; destruct s. inversion H0; simpl. replace (k - S i) with ((k - 1) - i) by omega. simpl; rewrite <- IHi. replace (S (k - 1)) with k by omega; reflexivity. omega. inversion H0. assert (1 <= k) by omega; omega. assert (1 <= k) by omega; omega. Qed.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass