proposition: Lemma permutation_sym : forall l m : seq A, permutation l m -> permutation m l.
proof: Proof. intros l1 l2 H'; elim H'. apply permutation_nil. intro a. apply permutation_singleton. intros. apply permutation_skip. exact H0. exact H2. exact H4. intros. apply permutation_swap. intros l1' l2' l3' H1 H2 H3 H4. apply permutation_trans with (1 := H4) (2 := H2). 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