Rel Dist floor bound iff complement bound

lemma relDist_floor_bound_iff_complement_bound (n upperBound : ℕ) (δ : ℝ≥0) :    n - Nat.floor (δ * (n)) ≤ upperBound ↔    (1 - δ) * (n : ℝ≥0) ≤ (upperBound : ℝ≥0) := by  let k := upperBound  set r : ℝ≥0 := δ * n  set m : ℕ := Nat.floor r  have h_m_le_r_NNReal : (m : NNReal) ≤ r := Nat.floor_le (a := r) (ha := zero_le)  have h_m_le_r_ENNReal : (m : ENNReal) ≤ (r : ENNReal) := by    change ( (m : NNReal) : ENNReal) ≤ (r : ENNReal)    rw [ENNReal.coe_le_coe]    exact h_m_le_r_NNReal  have hr : ↑m ≤ r := Nat.floor_le (mul_nonneg δ.coe_nonneg n.cast_nonneg)  have hr' : r < ↑m + 1 := Nat.lt_floor_add_one r  have h_sub : ↑(n - m) = max (↑n - ↑m) 0 := by    by_cases h : m ≤ n    · simp only [zero_le, sup_of_le_left]    · simp only [zero_le, sup_of_le_left]  conv_rhs => -- convert rhs to ENNReal    rw [←ENNReal.coe_le_coe, ENNReal.coe_mul, ENNReal.coe_sub,      ENNReal.coe_one, ENNReal.coe_natCast]    rw [ENNReal.sub_mul (h := fun h1 h2 => by exact ENNReal.natCast_ne_top n)]    simp only [one_mul, ENNReal.coe_natCast]  conv_lhs => -- convert lhs to ENNReal    rw [←Nat.cast_le (α := ENNReal) (m := n - m) (n := k)]    simp only [ENNReal.natCast_sub]  by_cases h_r_le_n : r ≤ n  · have h_m_le_n : m ≤ n := by exact Nat.floor_le_of_le h_r_le_n    constructor    · intro hNat_le      calc        _ ≤ (n : ENNReal) - (m : ENNReal) := by          rw [ENNReal.sub_le_sub_iff_left (b := ↑δ * ↑n) (c := (m : ENNReal))            (h := Nat.cast_le.mpr h_m_le_n) (h' := ENNReal.natCast_ne_top n)]          exact h_m_le_r_ENNReal        _ ≤ _ := by exact hNat_le    · intro hNNReal_le      -- APPROACH: Exploting the gap between any two consecutive Nat      let sub_eq := ENNReal.natCast_sub (m := n) (n := m)      rw [←sub_eq]      rw [Nat.cast_le]      rw [←Nat.lt_add_one_iff]      -- Convert to ℝ      rw [← Nat.cast_lt (α := ℝ)]      rw [Nat.cast_sub h_m_le_n, Nat.cast_add, Nat.cast_one]      -- The goal is now `(n : ℝ) - (m : ℝ) < (k : ℝ) + 1`      have h_hyp_ℝ : (n : ℝ) - (r : ℝ) ≤ (k : ℝ) := by        exact_mod_cast hNNReal_le      have h_floor_lt_ℝ : (r : ℝ) < (m : ℝ) + 1 := by        exact_mod_cast hr'      -- `linarith` proves `n - m < k + 1` from: `n - r ≤ k` AND `r < m + 1`      -- by showing `n - m < n - r + 1 ≤ k + 1`      linarith  · have h_n_lt_r : n < r := by exact lt_of_not_ge h_r_le_n    have h_m_ge_n : m ≥ n :=      NNReal.floor_ge_Nat_of_gt (r := r) (n := n) (h := lt_of_not_ge h_r_le_n)    have h_n_sub_m_eq_0 : n - m = 0 := Nat.sub_eq_zero_of_le h_m_ge_n    have h_n_sub_r_eq_0 : (n : ENNReal) - r = 0 := by      change ((n : NNReal) : ENNReal) - r = 0      rw [←ENNReal.coe_sub] -- ↑((n : ℝ≥0) - r) = 0      have h_n_sub_r_eq_0_NNReal : (n : NNReal) - r = 0 := by        apply NNReal.sub_eq_zero_of_le        exact le_of_lt h_n_lt_r      rw [h_n_sub_r_eq_0_NNReal]      exact rfl    conv_lhs => -- convert ↑n - ↑m into 0      rw [←ENNReal.natCast_sub]      rw [h_n_sub_m_eq_0, Nat.cast_zero]    conv_rhs => -- convert ↑n - ↑r into 0      change (n : ENNReal) - r ≤ k      rw [h_n_sub_r_eq_0]