feat(Order/Interval/Set/LinearOrder): add Ioi_diff_Ioc

Author: Deep0Thinking

Mathlib/Order/Interval/Set/LinearOrder.lean

@@ -547,6 +547,10 @@ theorem compl_Ioc : (Ioc a b)ᶜ = Iic a ∪ Ioi b := by
 theorem Iic_diff_Ioc : Iic b \ Ioc a b = Iic (a ⊓ b) := by
   grind
 
+@[simp]
+theorem Ioi_diff_Ioc : Ioi a \ Ioc a b = Ioi (max a b) := by
+  simp [diff_eq, compl_Ioc, inter_union_distrib_left, Ioi_inter_Iic, Ioi_inter_Ioi]
+
 theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : Iic b \ Ioc a b = Iic a := by
   grind