proposition: Lemma mat_gt_dec : rel_dec mat_gt.
proof: Proof. unfold mat_gt. apply mat_forall2_dec. exact gtx_dec. Defined.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)