Lemma lex_istrans (X:hSet) (Y:X->hSet) (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). contradicts pn k. 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. 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'. apply hdisj_in2; simpl. exists (idpath x). exact (Strans x y y' y'' s s'). 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.