CH2.LadderParams.lowerRectangle_subset_RposBar

lemma LadderParams.lowerRectangle_subset_RposBar (l : LadderParams) (n : ℕ) :    Rectangle ((l.σ n : ℂ) - (l.T : ℂ) * Complex.I) (1 - (l.δ : ℂ) * Complex.I) ⊆ l.RposBar := by  intro z hz  have hδ_le_T : -l.T ≤ -l.δ := by linarith [l.hδ.2, l.hT]  rcases (mem_Rect      (z := ((l.σ n : ℂ) - (l.T : ℂ) * Complex.I))      (w := (1 - (l.δ : ℂ) * 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.RposBar, 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⟩⟩