n : ℕ
c : CompositionAsSet n
⊢ Finset.min' c.boundaries (_ : Finset.Nonempty c.boundaries) = 0
n : ℕ
c : CompositionAsSet n
⊢ ↑(boundary c) { val := 0, isLt := (_ : 0 < Finset.card c.boundaries) } = 0
rw [boundary, Finset.orderEmbOfFin_zero rfl c.card_boundaries_pos]
no goals
n : ℕ
c : CompositionAsSet n
⊢ Finset.min' c.boundaries (_ : Finset.Nonempty c.boundaries) = 0
exact le_antisymm (Finset.min'_le _ _ c.zero_mem) (Fin.zero_le _)