∀ {α : Type u_1} {c : α} [inst : AddCommGroup α] [inst_1 : LinearOrder α] (x : α)
  (motive : (∃! k, 0 ≤ x - k • c ∧ x - k • c < c) → Prop) (x_1 : ∃! k, 0 ≤ x - k • c ∧ x - k • c < c),
  (∀ (n : ℤ) (H : 0 ≤ x - n • c ∧ x - n • c < c)
      (right : ∀ (y : ℤ), (fun k => 0 ≤ x - k • c ∧ x - k • c < c) y → y = n), motive ⋯) →
    motive x_1