Lemma EOge_le: ∏ x y : X, (x >= y) <-> (y <= x). Proof. now split. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.BinaryOperations