∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  (motive : (x : WithTop G) → x ≠ ⊤ → Prop) (x : WithTop G) (x_1 : x ≠ ⊤),
  (∀ (a : G) (x : ↑a ≠ ⊤), motive (some a) x) → motive x x_1