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