proposition: Lemma rev_fresh_seq : forall (s : seq A), fresh_seq s -> fresh_seq (rev s).
proof: Proof. intros; induction s. auto. rewrite rev_cons; apply rcons_fresh_seq; apply fresh_cons. inversion H; unfold sqfresh; apply insq; apply rev_fresh. unfold sqfresh in H2; by apply unsq. 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