Lemma tot_nle_iff_gt {X:hSet} (R:hrel X) : isTotalOrder R -> ∏ x y, ¬ (R x y) <-> R y x ∧ ¬ (y = x). Proof. intros i. assert (tot := pr2 i); simpl in tot. assert (refl := pr2 (pr1 (pr1 i))); simpl in refl. assert (anti := pr2 (pr1 i)); simpl in anti. split. { intros nle. split. - now apply tot_nge_to_le. - intros ne. induction ne. exact (nle (refl y)). } { intros yltx xley. induction yltx as [ylex neq]. exact (neq (anti _ _ ylex xley)). } Defined.
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.