proposition: Lemma nth_fresh : forall (s : seq K) (k c : nat), k < size s -> fresh_seq K s -> fresh K (take (k - c) s) (nth Zero s k).
proof: Proof. intros. induction c. assert (k - 0 = k) by omega. rewrite H1. assert (fresh_seq K (take (k + 1) s)). apply take_fresh_seq. exact H0. cut (take (k + 1) s = take k s ++ [:: nth Zero s k]). intro. rewrite H3 in H2. assert (fresh_seq K ((nth Zero s k) :: take k s)). apply fresh_seq_rcons. rewrite <- cat_rcons in H2. rewrite cats0 in H2. exact H2. apply unsq. inversion H4. unfold sqfresh in H7. exact H7. rewrite <- cat_rcons. rewrite cats0. rewrite <- take_nth. replace (S k) with (k + 1) by omega. reflexivity. apply (ssrbool.introT (P := S k <= size s)). apply ssrnat.leP. omega. cut (take (k - S c) s = take (k - S c) (take (k - c) s)). intro. rewrite H1. apply take_fresh. exact IHc. rewrite take_nest_redun. reflexivity. 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