proposition: Lemma dot_product_distr_l n (v vl vr : vec n) : dot_product (vl [+] vr) v =A= dot_product vl v + dot_product vr v.
proof: Proof. rewrite dot_product_comm, dot_product_distr_r, (dot_product_comm v vl), (dot_product_comm v vr). refl. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)