proposition: Lemma dot_product_distr_r : forall n (v vl vr : vec n), dot_product v (vl [+] vr) =A= dot_product v vl + dot_product v vr.
proof: Proof. induction n; intros. VOtac. unfold dot_product. simpl. ring. VSntac v. VSntac vl. VSntac vr. unfold dot_product. simpl. fold (Vtail vl [+] Vtail vr). fold (dot_product (Vtail v) (Vtail vl [+] Vtail vr)). rewrite IHn. unfold dot_product. ring. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)