{M : Type u_5} →
  [inst : AddCommMonoid M] →
    [inst_1 : PartialOrder M] →
      {motive : Archimedean M → Sort u} →
        (t : Archimedean M) → ((arch : ∀ (x : M) {y : M}, 0 < y → ∃ n, x ≤ n • y) → motive ⋯) → motive t