proposition: Lemma multiplicity_dropNth_neq: forall l p el el', nth_error l p = Some el' -> ~eqA el el' -> multiplicity (list_contents eqA_dec (drop_nth l p)) el = multiplicity (list_contents eqA_dec l) el.
proof: Proof. intros. rewrite !multiplicity_countIn. apply countIn_dropNth_neq with el'; trivial. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)