proposition: Lemma multiplicity_map_N_val_notin n i (hi : i>=n) : forall l : list (N n), multiplicity (list_contents eq_nat_dec (map N_val l)) i = 0.
proof: Proof. induction l; simpl. refl. rewrite IHl. destruct (eq_nat_dec a i). subst. destruct a as [a ha]. simpl in hi. lia. refl. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil) CoLoR(SortUtil RelUtil) CoLoR(ListPermutation)