proposition: Lemma ge_antisym : antisymmetric ge.
proof: Proof. intros m n mn nm. destruct mn; auto. destruct nm; auto. absurd (gt n m). apply gt_asym. hyp. hyp. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)