no goals
a b : ℝ
⊢ frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}
simpa only [closure_Ici, closure_Iic, frontier_Ici, frontier_Iic] using
  frontier_reProdIm (Ici a) (Iic b)