proposition: Lemma multiplicity_countIn: forall l el, multiplicity (list_contents eqA_dec l) el = countIn eqA eqA_dec el l.
proof: Proof. induction l; simpl; intros; trivial. destruct (eqA_dec a el); destruct (eqA_dec el a). rewrite IHl; lia. absurd (eqA el a); intuition. absurd (eqA a el); intuition. rewrite IHl; lia. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)