-ndefinition nat128 ≝ nat64 * nat2.
-ndefinition nat256 ≝ nat128 * nat2.
-ndefinition nat512 ≝ nat256 * nat2.
-ndefinition nat1024 ≝ nat512 * nat2.
-ndefinition nat2048 ≝ nat1024 * nat2.
-ndefinition nat4096 ≝ nat2048 * nat2.
-ndefinition nat8192 ≝ nat4096 * nat2.
-ndefinition nat16384 ≝ nat8192 * nat2.
-ndefinition nat32768 ≝ nat16384 * nat2.
-ndefinition nat65536 ≝ nat32768 * nat2.
+ndefinition nat128 ≝ nat64 + nat64.
+ndefinition nat256 ≝ nat128 + nat128.
+ndefinition nat512 ≝ nat256 + nat256.
+ndefinition nat1024 ≝ nat512 + nat512.
+ndefinition nat2048 ≝ nat1024 + nat1024.
+ndefinition nat4096 ≝ nat2048 + nat2048.
+ndefinition nat8192 ≝ nat4096 + nat4096.
+ndefinition nat16384 ≝ nat8192 + nat8192.
+ndefinition nat32768 ≝ nat16384 + nat16384.
+ndefinition nat65536 ≝ nat32768 + nat32768.