proposition: Lemma vector_plus_zero_r n (v : vec n) : v [+] zero_vec n =v v.
proof: Proof. apply Vforall2_intro_nth. intros. rewrite vector_plus_nth. set (w := Vnth_const A0 ip). fold zero_vec in w. rewrite w. ring. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)