proposition: Lemma ap_fresh_nth : forall (s : seq K) (k c : nat), 0 < k -> c < k -> k < size s -> fresh_seq K s -> (nth Zero s k) [-] (nth Zero s (k - S c)) [#] Zero.
proof: Proof. intros. apply minus_ap_zero. assert (fresh K (take (k - c) s) (nth Zero s k)). apply nth_fresh. exact H1. exact H2. assert (take (k - c) s = take (k - S c) s ++ [:: nth Zero s (k - S c)]). rewrite <- cat_rcons. rewrite <- take_nth. replace (S (k - S c)) with (k - c) by omega. rewrite cats0. reflexivity. apply (ssrbool.introT (P := S (k - S c) <= size s)). apply ssrnat.leP. omega. rewrite H3 in X. rewrite <- cat_rcons in X. rewrite cats0 in X. apply fresh_rcons in X. inversion X. algebra. 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