proposition: Lemma nf_multiplicity_big : forall l a c n , c < a -> nf (cons c n l) -> multiplicity a (cons c n l) = 0.
proof: Proof. induction l. inversion_clear 2. simpl; case (T1_eq_dec a c). intros; subst a; intros;absurd (lt c c);auto with T1. auto. simpl. intros. case (T1_eq_dec a c). intros; subst a; intros;absurd (lt c c);auto with T1. intro; case (T1_eq_dec a c). intro; subst a. case (lt_irr H);auto. intros; case (T1_eq_dec a l1). intro; absurd (lt a l1). rewrite <- e. subst l1. apply lt_irr. subst l1. inversion_clear H0;auto. eapply lt_trans;eauto. generalize (IHl2 a c n H). simpl. case (T1_eq_dec a c). intro; absurd (a=c);auto. intros. apply H1. inversion_clear H0. auto. inversion_clear H4. constructor;auto. constructor; auto. eapply lt_trans ; eauto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0