Definition concatenateFiniteOrderedSets {X:FiniteOrderedSet} (Y:X->FiniteOrderedSet) : 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.
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.