using cardinality for existence proof

Stream: maths

[Cody Bardin]

Hi there, I've introduced a type variables {α : Type*} [decidable_eq α] [monoid α] as well as a finset s over α. I want to prove the statement ∃ N : ℕ, ∀ w : list α, w.length ≥ N → has_sublist_prop w and wish to use the cardinality of s plus one to start, but I can't seem to understand why use ((s.card)+1) brings up an error message regarding has_add. Furthermore, if I remove the plus one, then it still fails to use s.card.