proposition: Lemma Vnth_V_aux : forall k (h : k<n) i (hi : i < S k), N_val (Vnth (V_aux h) hi) = k - i.
proof: Proof. induction k; simpl; intros; destruct i; simpl. refl. lia. refl. rewrite IHk. refl. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)