Lemma lex_istotal (X:hSet) (Y:X->hSet) (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.
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.