Johnson condition strong implies 2 le B card

lemma johnson_condition_strong_implies_2_le_B_card    (h_johnson : JohnsonConditionStrong B v) :    2 ≤ B.card := by  dsimp [JohnsonConditionStrong] at h_johnson  rcases eq : B.card with _ | card | _ <;> [simp_all; skip; omega]  obtain ⟨a, ha⟩ := card_eq_one.1 eq  replace h_johnson : 1 < |1 - (card F) / ((card F) - 1) * Δ₀(v, a) / (n : ℚ)| := by    simp_all [choose_2]  generalize eq₁ : card F = q  rcases q with _ | _ | q <;> [simp_all; simp_all; skip]  have h : (card F : ℚ) / (card F - 1) = 1 + 1 / (card F - 1) := by    have : (card F : ℚ) - 1 ≠ 0 := by simp [sub_eq_zero]; omega    field_simp    ring  have h' := JohnsonBound.abs_one_sub_div_le_one (v := v) (a := a) (by omega)  exact absurd (lt_of_lt_of_le (h ▸ h_johnson) h') (lt_irrefl _)