Lemma EOgt_lt: ∏ 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