{α : Type u} →
  [inst : LT α] →
    [inst_1 : Zero α] →
      [inst_2 : Add α] →
        {motive : Lean.Grind.ExistsAddOfLT α → Sort u_1} →
          ((exists_add_of_le : ∀ {a b : α}, a < b → ∃ c, 0 < c ∧ b = a + c) → motive ⋯) →
            (t : Lean.Grind.ExistsAddOfLT α) → motive t