proposition: Lemma perm_fresh : forall (s1 s2 : seq K), fresh_seq K s1 -> permutation K s1 s2 -> fresh_seq K s2.
proof: Proof. intros. induction H0. apply fresh_nil. apply fresh_cons. unfold sqfresh; simpl. apply insq; auto. apply fresh_nil. apply fresh_cons. assert (fresh_seq K (a :: s2)). apply IHpermutation2. apply fresh_cons. inversion H. inversion H2. inversion X. unfold sqfresh. apply insq. exact X1. inversion H. inversion H3. exact H7. inversion H. inversion H3. inversion X. unfold sqfresh. apply insq. simpl. split. exact X0. apply unsq. inversion H0. unfold sqfresh in H7. exact H7. apply IHpermutation3. inversion H. exact H3. apply fresh_cons. inversion H. inversion H2. inversion X. unfold sqfresh. apply insq. simpl. split. apply ap_symmetric. exact X0. apply unsq. inversion H3. unfold sqfresh in H6. exact H6. apply fresh_cons. inversion H. inversion H2. inversion X. unfold sqfresh. apply insq. exact X1. inversion H. inversion H3. exact H7. apply IHpermutation2. apply IHpermutation1. exact H. Qed.
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 bigopsClass