proposition: Lemma multiplicity_rw2 : forall a a' n' b', a <> a' -> multiplicity a (cons a' n' b') = multiplicity a b'.
proof: Proof. simpl. intros; case (T1_eq_dec a a'). intro; case H;auto. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0