proposition: Lemma dot_product_comm : forall n (u v : vec n), dot_product u v =A= dot_product v u.
proof: Proof. induction n. refl. intros. VSntac u. VSntac v. unfold dot_product. simpl. unfold dot_product in IHn. rewrite IHn. ring. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)