proposition: Lemma vector_plus_zero_l n (v : vec n) : zero_vec n [+] v =v v.
proof: Proof. rewrite vector_plus_comm. apply vector_plus_zero_r. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)