∀ {α : Type u_1} [inst : Preorder α] (motive : (x : WithZero α) → 0 ≤ x → (x x_1 : WithZero α) → x ≤ x_1 → Prop)
  (x : WithZero α) (x_1 : 0 ≤ x) (x_2 x_3 : WithZero α) (x_4 : x_2 ≤ x_3),
  (∀ (x : 0 ≤ 0) (a b : WithZero α) (x_5 : a ≤ b), motive none x a b x_5) →
    (∀ (x : α) (x_5 : 0 ≤ ↑x) (x_6 : WithZero α) (x_7 : 0 ≤ x_6), motive (some x) x_5 none x_6 x_7) →
      (∀ (x : α) (x_5 : 0 ≤ ↑x) (a : α) (h : ↑a ≤ 0), motive (some x) x_5 (some a) none h) →
        (∀ (x : α) (hx : 0 ≤ ↑x) (a b : α) (h : ↑a ≤ ↑b), motive (some x) hx (some a) (some b) h) →
          motive x x_1 x_2 x_3 x_4