E mul R div R sub 1 lt e add 1 real

lemma e_mul_R_div_R_sub_1_lt_e_add_1_real {e R : ℕ} (hR_gt_e_add_1 : e + 1 < R) :    ((e : ℝ) * (R : ℝ)) / ((R : ℝ) - 1) < (e : ℝ) + 1 := by  have hR_gt_one : R > 1 := by omega  have hR_Real_gt_one : (R : ℝ) > 1 := by exact Nat.cast_gt_Real_one R hR_gt_one  have h_R_gt_e_add_1_real : ((e + 1) : ℝ) < (R : ℝ) := by    rw [←Nat.cast_add_one (n := e)]    apply Nat.cast_lt (α := ℝ) (m := e + 1) (n := R).mpr hR_gt_e_add_1  have h_denom_pos : (R : ℝ) - 1 > 0 := by    -- `linarith` solves this from the hypothesis    linarith [hR_Real_gt_one]  -- 3. Use `div_lt_iff` to multiply the denominator across  -- This is the `ℝ` lemma for `a / b < c ↔ a < c * b` (since `b > 0`)  rw [div_lt_iff₀ (hc := h_denom_pos)]  -- Goal: ⊢ ↑e * ↑R < (↑e + 1) * (↑R - 1)  -- 4. THIS IS THE KEY STEP  -- Don't use `rw`. `linarith` will:  --   a) Expand the RHS to: `e*R - e + R - 1`  --   b) See the goal: `e*R < e*R - e + R - 1`  --   c) Cancel `e*R` from both sides: `0 < R - e - 1`  --   d) Rearrange: `e + 1 < R`  --   e) See this is exactly your hypothesis `h_R_gt_e_add_1_real`  linarith [h_R_gt_e_add_1_real]