proposition: Lemma multiplicity_L_aux n (i : N n) : forall k (kn : k < n), multiplicity (list_contents N_eq_dec (L_aux kn)) i = if le_dec i k then 1 else 0.
proof: Proof. destruct i as [i hi]; simpl. induction k; intro hk. simpl. destruct i. destruct (le_dec 0 0); lia. destruct (le_dec (S i) 0); lia. simpl. destruct i; rewrite IHk. destruct (le_dec 0 k); destruct (le_dec 0 (S k)); lia. destruct (eq_nat_dec k i); simpl; destruct (le_dec (S i) k); destruct (le_dec (S i) (S k)); lia. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil) CoLoR(SortUtil RelUtil) CoLoR(ListPermutation)