proposition: Lemma gt_dec : rel_dec gt.
proof: Proof. unfold rel_dec. intros. destruct x; destruct y; simpl; auto. destruct (gt_dec n n0); auto. Defined.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)