proposition: Lemma take_nest_redun : forall (n m : nat) (s : seq K), m <= n -> m <= size s -> take m (take n s) = take m s.
proof: Proof. intro n; induction n. intros m s H H0; rewrite take0; inversion H. repeat rewrite take0; reflexivity. intros m s H H0. destruct s. simpl; reflexivity. assert (take (S n) (s :: s0) = s :: take n s0) by auto. rewrite H1; destruct m. simpl; reflexivity. simpl; rewrite IHn. reflexivity. omega. inversion H0. auto. 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