proposition: Lemma arctic_dot_product_mon : forall i (v v' w w' : vector A i), vgt v v' -> vge w w' -> dot_product v w >_0 dot_product v' w'.
proof: Proof. unfold dot_product. induction v; intros; simpl. right. intuition. apply gtx_plus_compat. apply IHv. change v with (Vtail (Vcons h v)). apply Vforall2_tail. hyp. apply Vforall2_tail. hyp. apply gtx_mult_compat. change h with (Vhead (Vcons h v)). rewrite !Vhead_nth. apply Vforall2_elim_nth. hyp. rewrite !Vhead_nth. apply Vforall2_elim_nth. hyp. Qed.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)