proposition: Lemma Vnth_vec_of_val : forall n x (H : x < n), Vnth (vec_of_val n) H = xint x.
proof: Proof. intro n. elim n. intros x Hx. exfalso. apply (Nat.nlt_0_r Hx). intros p Hrec x H0. simpl vec_of_val. case (le_lt_eq_dec (le_S_n H0)); intro H1. rewrite (Vnth_addl (vec_of_val p) (xint p) H0 H1). apply Hrec. rewrite Vnth_addr. 2: hyp. rewrite H1. refl. Qed.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)