Gs sufficient multiplicity bound

lemma gs_sufficient_multiplicity_bound {dist : ℕ}    (hk : k + 1 ≤ n) (hm : 1 ≤ m) (h_dist : (dist : ℝ) / n < gs_johnson k n m) :  (gs_degree_bound k n m : ℝ) < m * (n - dist) := by    have h_mul : (m * (n - dist) : ℝ) > (m * n * (1 - gs_johnson k n m)) := by      rw [div_lt_iff₀] at h_dist <;> norm_num at * <;>        nlinarith [(by norm_cast : (k : ℝ) + 1 ≤ n), (by norm_cast : (1 : ℝ) ≤ m)]    refine lt_of_le_of_lt ?_ h_mul    refine le_trans (Nat.floor_le ?_) ?_    · positivity    · unfold gs_johnson; ring_nf; norm_num      norm_num [mul_assoc, mul_comm, mul_left_comm, ne_of_gt (zero_lt_one.trans_le hm)]