exact h_induc (B \ A).encard A B hA hB rfl
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
hA : A ⊆ B
hB : M.Indep B
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
h_induc : ∀ (n : ℕ∞), P n
⊢ M.relRank A B = (B \ A).encard
no goals