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