case h.e'_3
n : ℕ
c : CompositionAsSet n
⊢ Fin.last n = Finset.max' c.boundaries (_ : Finset.Nonempty c.boundaries)
n : ℕ
c : CompositionAsSet n
⊢ ↑(boundary c) { val := length c, isLt := (_ : length c < Finset.card c.boundaries) } = Fin.last n
convert Finset.orderEmbOfFin_last rfl c.card_boundaries_pos
no goals
case h.e'_3
n : ℕ
c : CompositionAsSet n
⊢ Fin.last n = Finset.max' c.boundaries (_ : Finset.Nonempty c.boundaries)
exact le_antisymm (Finset.le_max' _ _ c.getLast_mem) (Fin.le_last _)