proposition: Lemma multiplicity_InA : forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
proof: Proof. induction l. - simpl. split; inversion 1. - simpl. intros a'; split; intros H. + inversion_clear H. * apply (decide_left (eqA_dec a a')); auto with *. * destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto. + destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto. Qed.
imports: Lia Relations Multiset SetoidList