proposition: Lemma Vin_V_aux_elim x k (h : k<n) : Vin x (V_aux h) -> exists i, N_val x = k - i.
proof: Proof. intro xL. destruct (Vin_nth xL) as [i [i1 i2]]. apply N_eq in i2. rewrite Vnth_V_aux in i2. ex i. hyp. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)