proposition: Lemma meval_xi : forall n i (H : lt i n) (v : vec n), meval (mxi H) v = Vnth v H.
proof: Proof. induction n. intros. absurd (lt i 0). lia. hyp. intro. destruct i; intros; VSntac v. simpl. rewrite meval_one. ring. simpl. rewrite IHn. apply zeql. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)