Add Data.Nat.Binary.Base.divMod

[XiaohuWang0921]

Long division for Data.Nat.Binary as well as some related functions. This is still a draft. I will probably add some properties later.

[XiaohuWang0921]

Oops, did not see that _∸_ was already defined in Data.Nat.Binary.Subtraction. I simply removed my definition because it was not necessary to define long division anyway.
Though should I move my definition of _-_ also to Data.Nat.Binary.Subtraction? And perhaps also move divMod and related functions into a separate module? Frankly, I do not understand why there is a separate module just for subtraction and its properties in the first place.

[Taneb]

Thank you for this PR, this is definitely a worthwhile addition to the library. Have you managed to do any form of benchmarking?

[XiaohuWang0921]

@Taneb No, unfortunately I'm not very familiar with benchmarking.

[andreasabel]

CI reports failure: https://github.com/agda/agda-stdlib/actions/runs/5636154398/job/15267920707#step:10:654

/home/runner/work/agda-stdlib/agda-stdlib/src/Data/Nat/Binary/Properties.agda:149,53-54
Ambiguous name _%_. It could refer to any one of
  Data.Nat.Binary.Base._%_ bound at
    /home/runner/work/agda-stdlib/agda-stdlib/src/Data/Nat/Binary/Base.agda:146,1-4
  ℕ._%_ bound at
    /home/runner/work/agda-stdlib/agda-stdlib/src/Data/Nat/Base.agda:226,1-4
_%_ is in scope as
  * a defined name Data.Nat.Binary.Base._%_ brought into scope by
    - the opening of Data.Nat.Binary.Base at /home/runner/work/agda-stdlib/agda-stdlib/src/Data/Nat/Binary/Properties.agda:17,13-33
    - its definition at /home/runner/work/agda-stdlib/agda-stdlib/src/Data/Nat/Binary/Base.agda:146,1-4
  * a defined name Data.Nat.Base._%_ brought into scope by
    - the opening of Data.Nat.DivMod at /home/runner/work/agda-stdlib/agda-stdlib/src/Data/Nat/Binary/Properties.agda:19,13-28
    - the opening of Data.Nat.Base at
    - its definition at /home/runner/work/agda-stdlib/agda-stdlib/src/Data/Nat/Base.agda:226,1-4
when scope checking n % 2

[XiaohuWang0921]

@andreasabel Yep, it was nothing serious, just some naming conflicts in Data.Nat.Binary.Properties since it also imports from Data.Nat.DivMod. My latest commit fixed it.

[jamesmckinna]

What happened here?

[XiaohuWang0921]

@jamesmckinna I forgot this hasn't been merged and discarded my commits because there seemed to be conflicts with the upstream. Didn't know this happened. Sorry.