proposition: Lemma biggestUniqueness (X:OrderedSet) (x y:X) : isBiggest x -> isBiggest y -> x = y.
proof: 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 i. - apply OrderedSet_isantisymm. + now apply j. + assumption. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions