proposition: Lemma mat_arctic_mult_mon : mgt M M' -> mge N N' -> mgt (M <*> N) (M' <*> N').
proof: Proof. intros. unfold mat_forall2. intros. rewrite !mat_mult_spec. apply arctic_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: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)