# Library UniMath.Combinatorics.OrderedSets

partially ordered sets and ordered sets

Definition isTotalOrder {X : hSet} (R : hrel X) : hProp
:= make_hProp (isPartialOrder R × istotal R)
(isapropdirprod _ _ (isaprop_isPartialOrder R) (isaprop_istotal R)).

Section A.

Open Scope logic.

Lemma tot_nge_to_le {X:hSet} (R:hrel X) : istotal R x y, ¬ (R x y) R y x.
Proof.
intros tot ? ? nle.
now apply (hdisjtoimpl (tot x y)).
Defined.

Lemma tot_nle_iff_gt {X:hSet} (R:hrel X) :
isTotalOrder R x y, ¬ (R x y) R y x ¬ (y = x).
if R x y is x y, then this shows the equivalence of two definitions for 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.

End A.

Definition isSmallest {X : Poset} (x : X) : UU := y, x y.

Definition isBiggest {X : Poset} (x : X) : UU := y, y x.

Definition isMinimal {X : Poset} (x : X) : UU := y, y x x = y.

Definition isMaximal {X : Poset} (x : X) : UU := y, x y x = y.

Definition consecutive {X : Poset} (x y : X) : UU := x < y × z, ¬ (x < z × z < y).

Lemma isaprop_isSmallest {X : Poset} (x : X) : isaprop (isSmallest x).
Proof.
intros. unfold isSmallest. apply impred_prop.
Defined.

Lemma isaprop_isBiggest {X : Poset} (x : X) : isaprop (isBiggest x).
Proof.
intros. unfold isBiggest. apply impred_prop.
Defined.

Definition Poset_univalence_map {X Y:Poset} : X=Y PosetEquivalence X Y.
Proof. intros e. induction e. apply identityPosetEquivalence.
Defined.

Local Arguments isPosetEquivalence : clear implicits.
Local Arguments isaposetmorphism : clear implicits.

Lemma posetStructureIdentity {X:hSet} (R S:PartialOrder X) :
@isPosetEquivalence (X,,R) (X,,S) (idweq X) R=S.
Proof.
intros. split.
{ intros e.
apply subtypePath. { intros T. apply isaprop_isPartialOrder. }
induction R as [R r]; induction S as [S s]; simpl.
apply funextfun; intro x; apply funextfun; intro y.
unfold isPosetEquivalence in e.
unfold isaposetmorphism in e; simpl in e.
induction e as [e e'].
unfold posetRelation in ×. unfold invmap in *; simpl in ×.
apply hPropUnivalence. { apply e. } { apply e'. } }
{ intros p. induction p. apply isPosetEquivalence_idweq. }
Defined.

Local Lemma posetTransport_weq (X Y:Poset) : XY XY.
Proof.
intros. simple refine (weqbandf _ _ _ _).
{ apply hSet_univalence. }
intros e. apply invweq. induction X as [X R], Y as [Y S]; simpl in e.
induction e; simpl. apply weqimplimpl.
{ exact (pr1 (posetStructureIdentity R S)). }
{ exact (pr2 (posetStructureIdentity R S)). }
{ exact (isaprop_isPosetEquivalence _). }
{ exact (isaset_PartialOrder _ _ _). }
Defined.

Local Theorem Poset_univalence_0 (X Y:Poset) : X=Y XY.
Proof.
intros. intermediate_weq (XY).
- apply total2_paths_equiv.
- apply posetTransport_weq.
Defined.

Lemma Poset_univalence_compute {X Y:Poset} (e:X=Y) :
Poset_univalence_0 X Y e = Poset_univalence_map e.
Proof.
try reflexivity. Abort.

Theorem Poset_univalence (X Y:Poset) : X=Y XY.
Proof.
intros.
assert (k : pr1weq (Poset_univalence_0 X Y) ¬ @Poset_univalence_map X Y).
{ intro e. apply isinj_pr1_PosetEquivalence. induction e. reflexivity. }
exact (remakeweq k).
Defined.

Lemma Poset_univalence_compute {X Y:Poset} (e:X=Y) :
Poset_univalence X Y e = Poset_univalence_map e.
Proof. reflexivity. Defined.

Theorem PosetEquivalence_rect (X Y : Poset) (P : X Y UU) :
( e : X = Y, P (Poset_univalence_map e)) f, P f.
Proof.
intros ih ?.
set (p := ih (invmap (Poset_univalence _ _) f)).
set (h := homotweqinvweq (Poset_univalence _ _) f).
exact (transportf P h p).
Defined.

Ltac poset_induction f e :=
generalize f; apply PosetEquivalence_rect; intro e; clear f.

Lemma isMinimal_preserved {X Y:Poset} {x:X} (is:isMinimal x) (f:X Y) :
isMinimal (f x).
Proof.
intros.
poset_induction f e. induction e. simpl. exact is.
Defined.

Lemma isMaximal_preserved {X Y:Poset} {x:X} (is:isMaximal x) (f:X Y) :
isMaximal (f x).
Proof. intros. poset_induction f e. induction e. simpl. exact is.
Defined.

Lemma consecutive_preserved {X Y:Poset} {x y:X} (is:consecutive x y) (f:X Y) : consecutive (f x) (f y).
Proof. intros. poset_induction f e. induction e. simpl. exact is.
Defined.

# Ordered sets

see Bourbaki, Set Theory, III.1, where they are called totally ordered sets

Definition OrderedSet := X:Poset, istotal (posetRelation X).

Ltac unwrap_OrderedSet X :=
induction X as [X total];
induction X as [X _po_];
induction _po_ as [R _i_];
unwrap_isPartialOrder _i_;
unfold posetRelation in total;
simpl in total.

Local Definition underlyingPoset (X:OrderedSet) : Poset := pr1 X.
Coercion underlyingPoset : OrderedSet >-> Poset.

Declare Scope oset.
Delimit Scope oset with oset.

Definition Poset_lessthan {X:Poset} (x y:X) := x y × x != y .

Notation "X ≅ Y" := (PosetEquivalence X Y) (at level 60, no associativity) : oset.
Notation "m ≤ n" := (posetRelation _ m n) (no associativity, at level 70) : oset.
Notation "m <= n" := (posetRelation _ m n) (no associativity, at level 70) : oset.
Notation "m < n" := (Poset_lessthan m n) :oset.
Notation "n ≥ m" := (posetRelation _ m n) (no associativity, at level 70) : oset.
Notation "n >= m" := (posetRelation _ m n) (no associativity, at level 70) : oset.
Notation "n > m" := (Poset_lessthan m n) :oset.

Close Scope poset.
Local Open Scope oset.

Definition OrderedSet_isrefl {X:OrderedSet} (x:X) : x x.
Proof. intros. unwrap_OrderedSet X; simpl in x. apply refl. Defined.

Definition OrderedSet_isantisymm {X:OrderedSet} (x y:X) : x y y x x = y.
Proof. intros r s. unwrap_OrderedSet X; simpl in x, y. now apply antisymm. Defined.

Definition OrderedSet_istotal {X:OrderedSet} (x y:X): x y y x :=
pr2 X x y.

Lemma isdeceq_isdec_ordering (X:OrderedSet) : isdeceq X isdec_ordering X.
Proof.
intros deceq ? ?.
assert (tot := OrderedSet_istotal x y).
induction (deceq x y) as [j|j].
- apply ii1. induction j. unwrap_OrderedSet X. apply refl.
- assert (c : (y x) ⨿ (x y)).
{ assert (d : isaprop ((y x) ⨿ (x y))).
{ apply isapropcoprod.
× apply propproperty.
× apply propproperty.
× intros r s. apply j; clear j. unwrap_OrderedSet X. now apply antisymm. }
apply (squash_to_prop tot).
+ exact d.
+ intro e. exact e.
}
induction c as [c|c'].
+ now apply ii1.
+ apply ii2. intro le. apply j. now apply OrderedSet_isantisymm.
Defined.

Corollary isfinite_isdec_ordering (X:OrderedSet) : isfinite X isdec_ordering X.
Proof. intros i ? ?. apply isdeceq_isdec_ordering. now apply isfinite_isdeceq.
Defined.

Corollary isdeceq_isdec_lessthan (X:OrderedSet) :
isdeceq X (x y:X), decidable (x < y).
Proof.
intros i ? ?. unfold Poset_lessthan. apply decidable_ishinh. apply decidable_dirprod.
- now apply isdeceq_isdec_ordering.
- apply neg_isdecprop.
apply isdecpropif.
× apply setproperty.
× apply i.
Defined.

Corollary isfinite_isdec_lessthan (X:OrderedSet) : isfinite X (x y:X), decidable (x < y).
Proof. intros i ? ?. apply isdeceq_isdec_lessthan. now apply isfinite_isdeceq.
Defined.

Lemma isincl_underlyingPoset : isincl underlyingPoset.
Proof. apply isinclpr1. intros X. apply isaprop_istotal. Defined.

Definition underlyingPoset_weq (X Y:OrderedSet) :
X=Y (underlyingPoset X)=(underlyingPoset Y).
Proof.
Set Printing Coercions.
intros. simple refine (make_weq _ _).
{ apply maponpaths. }
apply isweqonpathsincl. apply isincl_underlyingPoset.
Unset Printing Coercions.
Defined.

Lemma smallestUniqueness (X:OrderedSet) (x y:X) : isSmallest x isSmallest y x = y.
Proof.
intros i j. assert (q := OrderedSet_istotal x y). apply (squash_to_prop q).
{ apply setproperty. }
intro c. induction c as [xley|ylex].
- apply OrderedSet_isantisymm.
+ assumption.
+ now apply j.
- apply OrderedSet_isantisymm.
+ now apply i.
+ assumption.
Defined.

Lemma biggestUniqueness (X:OrderedSet) (x y:X) : isBiggest x isBiggest y x = y.
Proof.
intros i j. assert (q := OrderedSet_istotal x y). apply (squash_to_prop q).
{ apply setproperty. }
intro c. induction c as [xley|ylex].
- apply OrderedSet_isantisymm.
+ assumption.
+ now apply i.
- apply OrderedSet_isantisymm.
+ now apply j.
+ assumption.
Defined.

Theorem OrderedSet_univalence (X Y:OrderedSet) : X=Y XY.
Proof. intros. exact ((Poset_univalence _ _) (underlyingPoset_weq _ _))%weq.
Defined.

Theorem OrderedSetEquivalence_rect (X Y : OrderedSet) (P : X Y UU) :
( e : X = Y, P (OrderedSet_univalence _ _ e)) f, P f.
Proof.
intros ih ?.
set (p := ih (invmap (OrderedSet_univalence _ _) f)).
set (h := homotweqinvweq (OrderedSet_univalence _ _) f).
exact (transportf P h p).
Defined.

Ltac oset_induction f e := generalize f; apply OrderedSetEquivalence_rect; intro e; clear f.

Definition FiniteOrderedSet := X:OrderedSet, isfinite X.
Definition underlyingOrderedSet (X:FiniteOrderedSet) : OrderedSet := pr1 X.
Coercion underlyingOrderedSet : FiniteOrderedSet >-> OrderedSet.
Definition finitenessProperty (X:FiniteOrderedSet) : isfinite X := pr2 X.
Definition underlyingFiniteSet : FiniteOrderedSet FiniteSet.
Proof. intros. X. apply finitenessProperty. Defined.
Coercion underlyingFiniteSet : FiniteOrderedSet >-> FiniteSet.

Lemma istotal_FiniteOrderedSet (X:FiniteOrderedSet) : istotal (posetRelation X).
Proof. intros. exact (pr2 (pr1 X)). Defined.

Lemma FiniteOrderedSet_isdeceq {X:FiniteOrderedSet} : isdeceq X.
Proof. intros. apply isfinite_isdeceq. apply finitenessProperty. Defined.

Lemma FiniteOrderedSet_isdec_ordering {X:FiniteOrderedSet} : isdec_ordering X.
Proof. intros. apply isfinite_isdec_ordering. apply finitenessProperty. Defined.

Definition FiniteOrderedSetDecidableOrdering (X:FiniteOrderedSet) : DecidableRelation X :=
λ (x y:X), decidable_to_DecidableProposition (FiniteOrderedSet_isdec_ordering x y).

Definition FiniteOrderedSetDecidableEquality (X:FiniteOrderedSet) : DecidableRelation X :=
λ (x y:X), @decidable_to_DecidableProposition (eqset x y) (FiniteOrderedSet_isdeceq x y).

Definition FiniteOrderedSetDecidableInequality (X:FiniteOrderedSet) : DecidableRelation X.
intros x y.
apply (@decidable_to_DecidableProposition (¬ (x = y)))%logic.
unfold decidable; simpl.
apply neg_isdecprop.
apply decidable_to_isdecprop_2.
{ apply setproperty. }
apply FiniteOrderedSet_isdeceq.
Defined.

Definition FiniteOrderedSetDecidableLessThan (X:FiniteOrderedSet) : DecidableRelation X.
intros x y. simple refine (decidable_to_DecidableProposition _).
- exact (x < y).
- apply isfinite_isdec_lessthan. apply finitenessProperty.
Defined.

Declare Scope foset.
Notation "x ≐ y" := (FiniteOrderedSetDecidableEquality _ x y) (at level 70, no associativity) : foset. Notation "x ≠ y" := (FiniteOrderedSetDecidableInequality _ x y) (at level 70, no associativity) : foset. Notation " x ≤ y " := ( FiniteOrderedSetDecidableOrdering _ x y ) (at level 70, no associativity) : foset. Notation " x <= y " := ( FiniteOrderedSetDecidableOrdering _ x y ) (at level 70, no associativity) : foset.
Notation " x ≥ y " := ( FiniteOrderedSetDecidableOrdering _ y x ) (at level 70, no associativity) : foset. Notation " x >= y " := ( FiniteOrderedSetDecidableOrdering _ y x ) (at level 70, no associativity) : foset.
Notation " x < y " := ( FiniteOrderedSetDecidableLessThan _ x y ) (at level 70, no associativity) : foset.
Notation " x > y " := ( FiniteOrderedSetDecidableLessThan _ y x ) (at level 70, no associativity) : foset.

Delimit Scope foset with foset.

Definition FiniteOrderedSet_segment {X:FiniteOrderedSet} (x:X) : FiniteSet.
intros. apply (@subsetFiniteSet X); intro y. exact (y < x)%foset.
Defined.

Definition height {X:FiniteOrderedSet} : X nat.
intros x. exact (cardinalityFiniteSet (FiniteOrderedSet_segment x)).
Defined.

Definition height_stn {X:FiniteOrderedSet} : X stn (cardinalityFiniteSet X).
Proof.
intros x.
(height x).

Abort.

making finite ordered sets in various ways

Definition standardFiniteOrderedSet (n:nat) : FiniteOrderedSet.
Proof.
intros. simple refine (_,,_).
- (stnposet n). intros x y; apply istotalnatleh.
- apply isfinitestn.
Defined.

Notation "⟦ n ⟧" := (standardFiniteOrderedSet n) : foset.

Lemma inducedPartialOrder {X Y} (f:XY) (incl:isInjective f) (R:hrel Y) (po:isPartialOrder R) :
isPartialOrder (λ x x' : X, R (f x) (f x')).
Proof.
intros.
split.
- split.
× intros x y z a b. exact (pr1 (pr1 po) (f x) (f y) (f z) a b).
× intros x. exact (pr2 (pr1 po) (f x)).
- intros x y a b. apply incl. exact (pr2 po (f x) (f y) a b).
Defined.

Corollary inducedPartialOrder_weq {X Y} (f:XY) (R:hrel Y) (po:isPartialOrder R) :
isPartialOrder (λ x x' : X, R (f x) (f x')).
Proof. intros. exact (inducedPartialOrder f (incl_injectivity f (weqproperty f)) R po). Defined.

Local Open Scope foset.
Definition transportFiniteOrdering {n} {X:UU} : X n FiniteOrderedSet.
Proof.
intros w.
simple refine (_,,_).
- simple refine (_,,_).
× simple refine (_,,_).
+ X. apply (isofhlevelweqb 2 w). apply setproperty.
+ unfold PartialOrder; simpl. simple refine (_,,_).
{ intros x y. exact (w x w y). }
apply inducedPartialOrder_weq.
exact (pr2 (pr2 (pr1 (pr1 ( n ))))).
× intros x y. apply (pr2 (pr1 ( n ))).
- simpl.
apply (isfiniteweqb w).
exact (pr2 ( n )).
Defined.
Close Scope foset.

concatenating finite ordered families of finite ordered sets

Definition lexicographicOrder
(X:hSet) (Y:XhSet)
(R:hrel X) (S : x, hrel (Y x)) : hrel ( x, Y x)%set.
intros u u'.
set (x := pr1 u). set (y := pr2 u). set (x' := pr1 u'). set (y' := pr2 u').
exact ((x != x' × R x x') ( e : x = x', S x' (transportf Y e y) y')).
Defined.

Lemma lex_isrefl (X:hSet) (Y:XhSet) (R:hrel X) (S : x, hrel (Y x)) :
( x, isrefl(S x)) isrefl (lexicographicOrder X Y R S).
Proof.
intros Srefl u. induction u as [x y]. apply hdisj_in2; simpl.
(idpath x). apply Srefl.
Defined.

Lemma lex_istrans (X:hSet) (Y:XhSet) (R:hrel X) (S : x, hrel (Y x)) :
isantisymm R istrans R ( x, istrans(S x)) istrans (lexicographicOrder X Y R S).
Proof.
intros Ranti Rtrans Strans u u' u'' p q.
induction u as [x y]. induction u' as [x' y']. induction u'' as [x'' y''].
refine (p _ _); clear p; intro p; simpl in p.
induction p as [p|p].
- induction p as [pn pl].
refine (q _ _); clear q; intro q; simpl in q.
induction q as [q|q].
+ apply hinhpr; simpl.
induction q as [qn ql].
apply ii1. split. intro ne. induction ne.
assert (k := Ranti x x' pl ql).
exact (Rtrans x x' x'' pl ql).
+ induction q as [e l].
apply hinhpr; simpl.
apply ii1.
induction e.
exact (pn,,pl).
- induction p as [e s].
induction e; unfold transportf in s; simpl in s; unfold idfun in s.
refine (q _ _); clear q; intro q; simpl in q.
induction q as [q|q].
+ induction q as [n r].
apply hdisj_in1; simpl.
exact (n,,r).
+ induction q as [e' s']. induction e'.
unfold transportf in s'; simpl in s'; unfold idfun in s'.
apply hdisj_in2; simpl.
(idpath x).
exact (Strans x y y' y'' s s').
Defined.

Local Ltac unwrap a := apply (squash_to_prop a);
[ apply isaset_total2_hSet | simpl; clear a; intro a; simpl in a ].

Lemma lex_isantisymm (X:hSet) (Y:XhSet) (R:hrel X) (S : x, hrel (Y x)) :
isantisymm R ( x, isantisymm(S x)) isantisymm (lexicographicOrder X Y R S).
Proof.
intros Ranti Santi u u' a b.
induction u as [x y]; induction u' as [x' y'].
unwrap a. unwrap b. induction a as [[m r]|a].
- induction b as [[n s]|b].
+ assert (eq := Ranti x x' r s). contradicts m eq.
+ induction b as [eq s]. contradicts (!eq) m.
- induction a as [eq s]. induction b as [[n r]|b].
induction b as [eq' s']. assert ( c : eq = !eq' ).
{ apply setproperty. }
induction (!c); clear c. induction eq'. assert ( t : y = y' ).
{ apply (Santi x' y y' s s'). }
induction t. reflexivity.
Defined.

Lemma lex_istotal (X:hSet) (Y:XhSet) (R:hrel X) (S : x, hrel (Y x)) :
isdeceq X istotal R ( x, istotal(S x)) istotal (lexicographicOrder X Y R S).
Proof.
intros Xdec Rtot Stot u u'. induction u as [x y]. induction u' as [x' y'].
induction (Xdec x x') as [eq|ne].
{ refine (Stot x' (transportf Y eq y) y' _ _); intro P. induction P as [P|P].
{ apply hdisj_in1. unfold lexicographicOrder; simpl. apply hdisj_in2. exact (eq,,P). }
{ apply hdisj_in2. unfold lexicographicOrder; simpl. apply hdisj_in2.
induction eq. exact (idpath _,,P). }}
{ refine (Rtot x x' _ _); intro P. induction P as [P|P].
{ apply hdisj_in1. apply hdisj_in1. simpl. exact (ne,,P). }
{ apply hdisj_in2. apply hdisj_in1. simpl. exact (ne pathsinv0,,P). }}
Defined.

Definition concatenateFiniteOrderedSets
{X:FiniteOrderedSet} (Y:XFiniteOrderedSet) : FiniteOrderedSet.
Proof.
intros.
simple refine (_,,_).
{
simple refine (_,,_).
{ simple refine (_,,_).
{ exact ( x, Y x)%set. }
simple refine (_,,_).
{ apply lexicographicOrder. apply posetRelation. intro. apply posetRelation. }
split.
{ split.
{ apply lex_istrans.
{ apply isantisymm_posetRelation. }
{ apply istrans_posetRelation. }
{ intro. apply istrans_posetRelation. } }
apply lex_isrefl.
intro; apply isrefl_posetRelation. }
apply lex_isantisymm.
{ apply isantisymm_posetRelation. }
intro. apply isantisymm_posetRelation. }
apply lex_istotal.
{ apply FiniteOrderedSet_isdeceq. }
{ apply istotal_FiniteOrderedSet. }
intro; apply istotal_FiniteOrderedSet. }
apply isfinitetotal2.
{ apply finitenessProperty. }
intro; apply finitenessProperty.
Defined.

Notation "'∑' x .. y , P" := (concatenateFiniteOrderedSets (λ x, .. (concatenateFiniteOrderedSets (λ y, P)) ..))
(at level 200, x binder, y binder, right associativity) : foset.

sorting finite ordered sets

Definition FiniteStructure (X:OrderedSet) := n, n %foset X.

Local Lemma std_auto n : iscontr ( n n ) %foset.
Proof.
intros. (identityPosetEquivalence _). intros f.
apply subtypePath.
{ intros g. apply isaprop_isPosetEquivalence. }
simpl. apply isinjpr1weq. simpl. apply funextfun. intros i.

Abort.

Lemma isapropFiniteStructure X : isaprop (FiniteStructure X).
Proof.
intros.
apply invproofirrelevance; intros r s.
destruct r as [m p].
destruct s as [n q].
apply subtypePairEquality.
{
intros k.
apply invproofirrelevance; intros [[r b] i] [[s c] j]; simpl in r,s,i,j.

}
{
apply weqtoeqstn.
exact (weqcomp (pr1 p) (invweq (pr1 q))).
}
Abort.

Theorem enumeration_FiniteOrderedSet (X:FiniteOrderedSet) : iscontr (FiniteStructure X).
Proof.
intros.
simple refine (_,,_).
{ (fincard (finitenessProperty X)).

Abort.

Theorem isasetFiniteOrderedSet : isaset FiniteOrderedSet.
Proof.

Abort.

# computably ordered sets

Local Open Scope logic.

Definition isLattice {X:hSet} (le:hrel X) (min max:binop X) :=
po : isPartialOrder le,
lub : x y z, le x z le y z le (max x y) z,
glb : x y t, le t x le t y le t (min x y),
unit.

Definition istrans2 {X:hSet} (le lt:hrel X) :=
transltle: x y z, lt x y le y z lt x z,
translelt: x y z, le x y lt y z lt x z,
unit.

Definition iswklin {X} (lt:hrel X) := x y z, lt x y lt x z lt z y.

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.
Let eq x y := @eqset X x y.
Let ne x y := hneg (eq 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.

Local Lemma lt_implies_le x y : lt x y le x y.
Proof.
intros l.
intro m.
expand ic.
assert (n := translt _ _ _ l m).
exact (irrefl _ n).
Defined.

Local Lemma apart_implies_ne x y : apart x y ne x y.
Proof.
expand ic.
intros a e.
induction e.
apply (apart_isirrefl _ a).
Defined.

Local Lemma tightness x y : ¬ apart x y x = y.
Proof.
expand ic.
split.
- intro m. assert (p := fromnegcoprod_prop m); clear m.
induction p as [p q]. now apply antisymmle.
- intro e. induction e. apply apart_isirrefl.
Defined.

Local Lemma ne_implies_dnegapart x y : ne x y ¬¬ apart x y.
Proof.
intros n m.
refine (n _); clear n.
now apply tightness.
Defined.

Section ClassicalProperties.

Variable lem:LEM.

Local Lemma ne_implies_apart x y : ne x y apart x y.
Proof.
intros a.
apply (dneg_LEM _ lem).
now apply ne_implies_dnegapart.
Defined.

Local Lemma trichotomy x y : lt x y eq x y lt y x.
Proof.
intros.
induction (lem (eq x y)) as [a|b].
- apply hdisj_in2; apply hdisj_in1; exact a.
- assert (l := ne_implies_apart _ _ b); clear b.
unfold apart in l.
refine (l _ _); intro m; clear l.
induction m as [n|o].
× apply hdisj_in2; apply hdisj_in2; exact n.
× apply hdisj_in1; exact o.
Defined.

Local Lemma le_istotal : istotal le.
Proof.
intros x y.
assert (m := trichotomy x y).
refine (m _ _); clear m; intro m; induction m as [m|m].
- apply hdisj_in1. apply lt_implies_le. exact m.
- refine (m _ _); clear m; intro m; induction m as [m|m].
× apply hdisj_in1. induction m. unfold le. expand ic. apply irrefl.
× apply hdisj_in2. apply lt_implies_le. exact m.
Defined.

End ClassicalProperties.

End OtherProperties.