proposition: Lemma multiplicity_rw1 : forall a n b, multiplicity a (cons a n b) = (S n + multiplicity a b)%nat.
proof: Proof. simpl. intros; case (T1_eq_dec a a). auto. intro; absurd (a=a);auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0