@[simp]

theorem Set.inv_Icc {α : Type u_1} [OrderedCommGroup α] (a b : α) : (Set.Icc a b)⁻¹ = Set.Icc b⁻¹ a⁻¹

@[simp]

theorem Set.neg_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Set.Icc a b = Set.Icc (-b) (-a)

@[simp]

theorem Set.smul_Icc {α : Type u_1} [LinearOrderedCommMonoid α] [MulLeftReflectLE α] [ExistsMulOfLE α] (a b c : α) : a • Set.Icc b c = Set.Icc (a * b) (a * c)

@[simp]

theorem Set.vadd_Icc {α : Type u_1} [LinearOrderedAddCommMonoid α] [AddLeftReflectLE α] [ExistsAddOfLE α] (a b c : α) : a +ᵥ Set.Icc b c = Set.Icc (a + b) (a + c)

theorem Set.Icc_mul_Icc {α : Type u_1} [LinearOrderedCommMonoid α] [MulLeftReflectLE α] [ExistsMulOfLE α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : Set.Icc a b * Set.Icc c d = Set.Icc (a * c) (b * d)

theorem Set.Icc_add_Icc {α : Type u_1} [LinearOrderedAddCommMonoid α] [AddLeftReflectLE α] [ExistsAddOfLE α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : Set.Icc a b + Set.Icc c d = Set.Icc (a + c) (b + d)