proposition: Lemma multiplicity_map_N_val n i (hi : i<n) : forall l, multiplicity (list_contents eq_nat_dec (map N_val l)) i = multiplicity (list_contents N_eq_dec l) (N_ hi).
proof: Proof. induction l; simpl. refl. rewrite IHl. destruct a as [j hj]; simpl. destruct (eq_nat_dec j i); refl. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil) CoLoR(SortUtil RelUtil) CoLoR(ListPermutation)