proposition: Lemma gt_dec : rel_dec gt.
proof: Proof. intros x y. destruct x; destruct y; simpl; auto. destruct (Z_lt_dec z0 z); [left | right]; lia. Defined.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)