proposition: Lemma gtx_dec : rel_dec gtx.
proof: Proof. intros x y. destruct (gt_dec x y). left. left. hyp. destruct (eqA_dec x MinusInf). destruct (eqA_dec y MinusInf). left. right. auto. right. unfold gtx. intuition. right. unfold gtx. intuition. Defined.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)