proposition: Lemma fresh_seq_rcons : forall (s : seq A) (a : A), fresh_seq (rcons s a) -> fresh_seq (a :: s).
proof: Proof. intros; induction s. auto. simpl in H; inversion H; apply fresh_cons. unfold sqfresh; apply insq. assert (fresh (a :: s) t); apply fresh_rcons. unfold sqfresh in H2; by apply unsq in H2. simpl; simpl in X; inversion X; apply unsq; inversion H. assert (fresh_seq (a :: s)). by apply IHs. apply insq; apply rcons_fresh; simpl; split. algebra. apply unsq; inversion H8. unfold sqfresh in H11; apply unsq in H11; by apply insq. apply fresh_cons; unfold sqfresh in H2; apply unsq in H2. apply fresh_rcons in H2; inversion H2; unfold sqfresh. by apply insq. assert (fresh_seq (a :: s)). by apply IHs. by inversion H4. 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