proposition: Lemma tot_nle_iff_gt {X:hSet} (R:hrel X) : isTotalOrder R -> ∏ x y, ¬ (R x y) <-> R y x ∧ ¬ (y = x).
proof: 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.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions