Lemma smallestUniqueness (X:OrderedSet) (x y:X) : isSmallest x -> isSmallest y -> x = y. Proof. intros i j. assert (q := OrderedSet_istotal x y). apply (squash_to_prop q). { apply setproperty. } intro c. induction c as [xley|ylex]. - apply OrderedSet_isantisymm. + assumption. + now apply j. - apply OrderedSet_isantisymm. + now apply i. + assumption. 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.