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