proposition: Lemma permutation_one_inv : forall (a : A) (l : seq A), permutation (a :: nil) l -> l = a :: nil.
proof: Proof. intros a l H; apply permutation_one_inv_aux with (l1 := a :: nil); auto. 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