proposition: Lemma ge_antisym : antisymmetric ge.
proof: Proof. intros x y xy yx. destruct xy. destruct yx. absurd (gt y x). apply gt_asym. hyp. hyp. auto. hyp. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)