Expand description
Lean’s natural numbers on top of logicaffeine_base::BigInt.
BigInt supplies the arithmetic; this wrapper supplies Nat’s semantics — values never go
negative, subtraction truncates at zero, and n / 0 = 0, n % 0 = n — so the kernel’s
literal extension computes exactly what Lean’s Nat definitions compute.