proposition: Lemma nf_multiplicity_head : forall l c n , nf (cons c n l) -> multiplicity c (cons c n l) = S n.
proof: Proof. induction l. simpl. intros; case (T1_eq_dec c c). auto with arith. intros; absurd (c=c); auto. intros;case (T1_eq_dec c c). 2: intros;absurd (c=c);auto. case (T1_eq_dec c l1); simpl. assert (c <> l1). red; intro; subst l1. case (lt_irr (a:=c)). inversion_clear H;auto. intros; absurd (c=l1);auto. assert (nf (cons c n0 l2)). generalize H;induction l2. constructor. inversion H;auto. constructor. inversion H;auto. apply lt_trans with l1;auto. inversion H8;auto. inversion H0;auto. inversion H0. inversion H8;auto. intros; case (T1_eq_dec c c). case (T1_eq_dec c l1). intro;case n1;auto. replace (multiplicity c l2) with 0. auto with arith. generalize H0;elim l2. simpl;auto. intros. simpl. case (T1_eq_dec c t). intro. subst t; inversion H3. case (lt_irr H7). intro;apply H2. generalize H3;case t0. constructor;auto. inversion H3;auto. constructor;auto. inversion H4. apply lt_trans with t;auto. inversion H12;auto. inversion H4;auto. inversion H4. inversion H12;auto. intro H1;case H1;auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0