proposition: Lemma dot_product_cons : forall n al ar (vl vr : vec n), dot_product (Vcons al vl) (Vcons ar vr) =A= al * ar + dot_product vl vr.
proof: Proof. intros. unfold dot_product. simpl. ring. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)