no goals
ι : Type ?u.386687
α : Type u_1
inst✝ : OrderedAddCommGroup α
s t : Interval α
a : α
x✝ : Interval α
⊢ length (⊥ + x✝) ≤ length ⊥ + length x✝
simp
no goals
ι : Type ?u.386687
α : Type u_1
inst✝ : OrderedAddCommGroup α
s t : Interval α
a : α
x✝ : Interval α
⊢ length (x✝ + ⊥) ≤ length x✝ + length ⊥
simp