proposition: Lemma nodup_L_aux {n} : forall k (hk : k < n), nodup (L_aux hk).
proof: Proof. induction k; intro hk; simpl. tauto. split. 2: apply IHk. intro h. destruct (In_L_aux_elim h) as [i e]. simpl in e. lia. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)