proposition: Lemma dot_product_zero : forall n (v v' : vec n), Vforall (fun el => el =A= A0) v -> dot_product v v' =A= A0.
proof: Proof. induction n; intros. VOtac. refl. VSntac v. VSntac v'. unfold dot_product. simpl. fold (dot_product (Vtail v) (Vtail v')). rewrite IHn. assert (Vhead v =A= A0). rewrite Vhead_nth. apply Vforall_nth. hyp. rewrite H2. ring. apply Vforall_incl with (S n) v. intros. apply Vin_tail. hyp. hyp. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)