exact ((tsub_le_self).trans_lt (WithTop.coe_lt_top k)).ne
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ ↑k - (E ∩ C).encard ≠ ⊤
no goals