CH2.LadderParams.upperRectangle_subset_Rpos

lemma LadderParams.upperRectangle_subset_Rpos (l : LadderParams) (n : ℕ) :    Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) ⊆ l.Rpos := by  intro z hz  have hδ_le_T : l.δ ≤ l.T := by    have hδ := l.hδ.2    have hT : 0 < l.T := l.hT    linarith  rcases (mem_Rect      (z := ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I))      (w := (1 + (l.T : ℂ) * Complex.I))      (p := z)      (zRe_lt_wRe := by simpa using l.hσ n)      (zIm_lt_wIm := by simpa using hδ_le_T)).1 hz with    ⟨hz_re_left, hz_re_right, hz_im_bot, hz_im_top⟩  simp only [LadderParams.Rpos, Set.mem_setOf_eq, Set.mem_Icc]  exact ⟨by simpa using hz_re_right, ⟨by simpa using hz_im_bot, by simpa using hz_im_top⟩⟩