proposition: Lemma permutation_nil_inv : forall l : seq A, permutation l nil -> l = nil.
proof: Proof. intros l H; generalize (permutation_size _ _ H); case l; simpl in |- *; auto. intros; discriminate. 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