proposition: Lemma permutation_one_inv_aux : forall l1 l2 : seq A, permutation l1 l2 -> forall a : A, l1 = a :: nil -> l2 = a :: nil.
proof: Proof. intros l1 l2 H; elim H; clear H l1 l2; auto. intros. inversion H5. intros. inversion 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