proposition: Lemma dot_product_mon : forall i (v v' w w' : vec i), v >=v v' -> w >=v w' -> dot_product v w >>= dot_product v' w'.
proof: Proof. unfold dot_product. induction v. auto with arith. intros. simpl. apply plus_ge_compat. apply IHv. change v with (Vtail (Vcons h v)). apply Vforall2_tail. hyp. apply Vforall2_tail. hyp. set (p0 := Nat.lt_0_succ n0). apply mult_ge_compat. change h with (Vnth (Vcons h v) p0). rewrite Vhead_nth. apply Vforall2_elim_nth. hyp. rewrite !Vhead_nth. apply Vforall2_elim_nth. hyp. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)