α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)
simp_rw [add_comm _ c]
no goals
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)
exact map_add_left_Icc _ _ _