proposition: Lemma nf_multiplicity_tail : forall l a c n , a < c -> nf (cons c n l) -> multiplicity a (cons c n l) = multiplicity a l.
proof: Proof. inversion_clear 2. simpl;case (trichotomy_inf a c). destruct 1. case (T1_eq_dec a c). intro; subst a; absurd (lt c c);auto with T1. auto. case (T1_eq_dec a c). intro; subst a; absurd (lt c c);auto with T1. auto . case (T1_eq_dec a c). intro; subst a; absurd (lt c c);auto with T1. auto. simpl. case (T1_eq_dec a c). case (T1_eq_dec a a'). intro; subst a; intros;absurd (lt c c);auto with T1. subst c;auto. intros; subst a; intros;absurd (lt c c);auto with T1. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0