Definition isComputablyOrdered {X:hSet} (lt:hrel X) (min max:binop X) := let le x y := ¬ lt y x in ∑ latt: isLattice le min max, ∑ trans2: istrans2 le lt, ∑ translt: istrans lt, ∑ irrefl: isirrefl lt, ∑ cotrans: iscotrans lt, unit. Local Ltac expand ic := induction ic as [[[[transle reflle]antisymmle][lub[glb _]]] [[transltle [translelt _]][translt[irrefl[cotrans _]]]]]. Section OtherProperties. Variable (X:hSet) (lt:hrel X) (min max:binop X) (ic:isComputablyOrdered lt min max). Let le x y := ¬ lt y x. Let apart x y := lt y x ∨ lt x y. Local Lemma apart_isirrefl : isirrefl apart. Proof. expand ic. intros x a. unfold apart in a. apply (a hfalse); clear a; intros b. induction b as [b|b]; exact (irrefl _ b). 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.