Almost johnson choose 2 elimed

lemma almost_johnson_choose_2_elimed [Zero F]    (h_n : 0 < n) (h_B : 2 ≤ B.card) (h_card : 2 ≤ card F) :    (k B * (k B - 1) +      (B.card - k B) * ((B.card - k B) / (card F - 1) - 1)) ≤    B.card * (B.card - 1) * (n - d B) / n := by  have h_expand : (card F - 1 : ℚ) ≠ 0 := sub_ne_zero_of_ne (by norm_cast; linarith)  have h_expand : (2 : ℚ) * choose_2 (k B) + (2 : ℚ) * ((card F - 1) : ℚ) *      choose_2 ((B.card - k B) / (card F - 1)) ≤        (2 : ℚ) * choose_2 B.card * (n - d B) / n := by    have h_expand : (2 : ℚ) * choose_2 (k B) + (2 : ℚ) * ((card F - 1) : ℚ) *        choose_2 ((B.card - k B) / (card F - 1)) ≤          (2 : ℚ) * choose_2 B.card * (n - d B) / n := by      have := almost_johnson h_n h_B h_card      rw [le_div_iff₀] <;> first | positivity | linarith    convert h_expand using 1  convert h_expand using 1 <;> push_cast [choose_2] <;> ring_nf!  grind +ring