∀ (A : Type u_1) (α : Type u_2) [inst : AddMonoid A] [inst_1 : SMul α A] [inst_2 : Zero α]
  (H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => n • a),
  divisibleByOfSMulRightSurj A α H =
    { div := fun a n => if x : n = 0 then 0 else ⋯.choose, div_zero := ⋯, div_cancel := ⋯ }