Lemma lex_isantisymm (X:hSet) (Y:X->hSet) (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]. { contradicts n (!eq). } 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.
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.