English
If a ≤ succ(b), then the closed interval [a, succ(b)] equals {succ(b)} union [a, b].
Русский
Если a ≤ succ(b), то пара Closed интервал [a, succ(b)] равен {succ(b)} ∪ [a, b].
LaTeX
$$$\text{If } a \leq \operatorname{succ} b:\; \mathrm{Icc}(a, \operatorname{succ} b) = \operatorname{insert}(\operatorname{succ} b)(\mathrm{Icc}(a, b))$$$
Lean4
theorem Icc_succ_right (h : a ≤ succ b) : Icc a (succ b) = insert (succ b) (Icc a b) := by
simp_rw [← Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]