proposition: Lemma take_fresh_seq : forall (n : nat) (s : seq A), fresh_seq s -> fresh_seq (take n s).
proof: Proof. intro n; induction n. intros s H; simpl; rewrite take0; exact fresh_nil. intros s H; destruct s; simpl; auto. simpl; apply fresh_cons. unfold sqfresh; apply insq; apply take_fresh. apply unsq; by inversion H. apply IHn; by inversion H. Defined.
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