lift k to ℕ using hk
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ∞
hk : k ≠ ⊤
⊢ unifOn E k ／ C = unifOn (E \ C) (k - (E ∩ C).encard)
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
⊢ unifOn E ↑k ／ C = unifOn (E \ C) (↑k - (E ∩ C).encard)