proposition: Lemma ge_dec : rel_dec ge.
proof: Proof. intros x y. destruct (gt_dec x y). left. left. trivial. destruct (eqA_dec x y). left. right. trivial. right. intro xy. destruct xy; auto. Defined.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)