proposition: Lemma in_multiplicity: forall l a, In a l -> multiplicity (list_contents eqA_dec l) a > 0.
proof: Proof. induction l; simpl; intros. lia. destruct H. destruct (eqA_dec a a0). lia. absurd (eqA a a0); trivial. rewrite H; intuition. set (w := IHl a0 H); lia. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)