lift k to ℕ using hktop
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hktop : k ≠ ⊤
hk : k ≤ E.encard
hBE : B ⊆ E
⊢ (unifOn E k).Base B ↔ B.encard = k
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hBE : B ⊆ E
k : ℕ
hk : ↑k ≤ E.encard
⊢ (unifOn E ↑k).Base B ↔ B.encard = ↑k