∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] {a b c d : α} (x : α)
  (motive : x ∈ Set.Icc (a + c) (b + d) → Prop) (x_1 : x ∈ Set.Icc (a + c) (b + d)),
  (∀ (hacx : a + c ≤ x) (hxbd : x ≤ b + d), motive ⋯) → motive x_1