proposition: Lemma mat_vec_prod_gt_compat : forall (M M' : mat) m m', mat_gt M M' -> m >=v m' -> vec_gt (mat_vec_prod M m) (mat_vec_prod M' m').
proof: Proof. intros. unfold mat_vec_prod, vec_gt. apply Vforall2_intro_nth. intros. rewrite !Vnth_col_mat. apply mat_arctic_mult_mon. hyp. intros k l pk pl. rewrite !vec_to_col_mat_spec. apply Vforall2_elim_nth. hyp. Qed.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)