proposition: Lemma vector_plus_comm n (v1 v2 : vec n) : v1 [+] v2 =v v2 [+] v1.
proof: Proof. apply Vforall2_intro_nth. intros. rewrite !vector_plus_nth. ring. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)