fact: Definition gt m n := match m, n with | PlusInf, PlusInf => False | PlusInf, _ => True | TPos _, PlusInf => False | TPos m, TPos n => m > n end.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)