(**************************************************************************)
include "ground/notation/functions/downarrow_1.ma".
-include "ground/arith/pnat_dis.ma".
+include "ground/arith/pnat_split.ma".
include "ground/arith/nat.ma".
(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
(*** pred *)
definition npred (m): nat ≝ match m with
[ nzero ⇒ 𝟎
-| ninj p ⇒ pdis … (𝟎) ninj p
+| ninj p ⇒ psplit … (𝟎) ninj p
].
interpretation