proposition: 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: 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.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions