proposition: Lemma mat_vec_prod_ge_compat : forall i j (M M' : matrix i j) m m', mat_ge M M' -> m >=v m' -> mat_vec_prod M m >=v mat_vec_prod M' m'.
proof: Proof. intros. unfold mat_vec_prod. apply Vforall2_intro_nth. intros. rewrite !Vnth_col_mat. apply mat_mult_mon. hyp. unfold mat_ge. intros k l pk pl. rewrite !vec_to_col_mat_spec. apply Vforall2_elim_nth. hyp. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)