[Agda] original Nat

[Sergei Meshveliani]

Please, what is a regular way to switch between the built-in Nat
arithmetic and the original one (implemented in Agda) ?

Data.Nat.Base  of  lib-0.14  contains

 open import Agda.Builtin.Nat public using ( zero; suc; _+_; _*_ )
                                     renaming ( Nat to ℕ; _-_ to _∸_ )

But I do not find the module  Agda.Builtin.Nat.

I need to use the Nat arithmetic programmed in Agda
(ℕ; _+_, _*_, _∸_, _≤_ ...) as in early days.

Thanks,

------
Sergei