proposition: Lemma multiplicity_L n (i : N n) : multiplicity (list_contents N_eq_dec (L n)) i = 1.
proof: Proof. destruct n as [|n]. apply any_of_N0. hyp. unfold L. rewrite multiplicity_L_aux. destruct (le_dec i n). refl. destruct i as [i hi]. simpl in n0. lia. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil) CoLoR(SortUtil RelUtil) CoLoR(ListPermutation)