proposition: Lemma vector_plus_nth n (vl vr : vec n) i (ip : i < n) : Vnth (vl [+] vr) ip =A= Vnth vl ip + Vnth vr ip.
proof: Proof. unfold vector_plus. rewrite Vnth_map2. refl. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)