proposition: Lemma dot_product_distr_mult : forall n a (v v' : vec n), a * dot_product v v' =A= dot_product (Vbuild (fun i ip => a * Vnth v ip)) v'.
proof: Proof. induction n; intros. VOtac. unfold dot_product. simpl. ring. rewrite (VSn_eq (Vbuild (fun i (ip : i < S n) => a * Vnth v ip))). VSntac v. VSntac v'. rewrite !dot_product_cons. ring_simplify. rewrite IHn, Vbuild_tail, Vbuild_head. simpl. ring_simplify. match goal with |- _ + dot_product ?X _ =A= _ + dot_product ?Y _ => replace X with Y end. refl. apply Veq_nth. intros. rewrite !Vbuild_nth, lt_Sn_nS. refl. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)