proposition: Lemma nfs_to_nf : forall l a, nfs l -> (0 < multiplicity a l)%nat -> nf a.
proof: Proof. induction l. simpl. inversion 2. simpl. intros; case (T1_eq_dec a l1). intro; subst a. inversion H;auto. generalize H0; case (T1_eq_dec a l1). intros; absurd (a=l1);auto. intros. apply IHl2. inversion H. auto. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0