proposition: Lemma multiplicity_nats_decr_lt i : forall n, multiplicity (list_contents eq_nat_dec (nats_decr_lt n)) i = if lt_ge_dec i n then 1 else 0.
proof: Proof. induction n; simpl. destruct (lt_ge_dec i 0); lia. rewrite IHn. destruct (lt_ge_dec i n); destruct (eq_nat_dec n i); destruct (lt_ge_dec i (S n)); lia. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil) CoLoR(SortUtil RelUtil) CoLoR(ListPermutation)