proposition: Lemma mat_mult_mon : M >=m M' -> N >=m N' -> M <*> N >=m M' <*> N'.
proof: Proof. intros. unfold mat_ge, mat_forall2. intros. rewrite !mat_mult_spec. apply dot_product_mon. apply Vforall2_intro_nth. intros. exact (H i i0 ip ip0). apply Vforall2_intro_nth. intros. rewrite <- !get_elem_swap. exact (H0 i0 j ip0 jp). Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)