proposition: Lemma rcons_fresh : forall (s : seq A) (a t : A), fresh (t :: s) a -> fresh (rcons s t) a.
proof: Proof. intros s a t H; induction s. simpl; by inversion H. simpl; inversion H; inversion X0; split. auto. apply IHs; simpl; by split. 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