Relative Unique Decoding Radius RS eq

theorem relativeUniqueDecodingRadius_RS_eq [Fintype ι]  {α : ι ↪ F} [Field F] [DecidableEq F] [NeZero n]  (h : n ≤ Fintype.card ι) :  Code.relativeUniqueDecodingRadius (ι := ι) (F := F) (C := ReedSolomon.code α n) =    ((1 : ℝ≥0) - n / Fintype.card ι) / 2 := by  have h_card_ne_zero: Fintype.card ι ≠ 0 := by    by_contra h_card_eq_zero    have h_n_eq_0 : n = 0 := by omega    have h_n_ne_0 : n ≠ 0 := by exact Ne.symm (NeZero.ne' n)    exact h_n_ne_0 h_n_eq_0  rw [Code.relativeUniqueDecodingRadius, ReedSolomon.dist_eq_of_le h]  simp only [Nat.cast_add, Nat.cast_tsub, Nat.cast_one, add_tsub_cancel_right]  conv_lhs =>    rw [NNReal.sub_div, NNReal.sub_div, div_div, mul_comm, ←div_div]    rw [div_self (Nat.cast_ne_zero.mpr h_card_ne_zero)]  conv_rhs => rw [NNReal.sub_div, div_div, mul_comm, ←div_div]