proposition: Lemma nth_L_aux x : forall k (h : k<n) i, i <= k -> N_val (nth i (L_aux h) x) = k - i.
proof: Proof. induction k; simpl; intros; destruct i; simpl. refl. lia. refl. rewrite IHk. refl. lia. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)