(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
+definition pnpred (p): nat ≝
+ psplit … (𝟎) ninj p.
+
+interpretation
+ "positive predecessor (non-negative integers)"
+ 'DownArrow p = (pnpred p).
+
(*** pred *)
definition npred (m): nat ≝ match m with
[ nzero ⇒ 𝟎
-| ninj p ⇒ psplit … (𝟎) ninj p
+| ninj p ⇒ ↓p
].
interpretation
lemma npred_zero: 𝟎 = ↓𝟎.
// qed.
+lemma npred_inj (p): ↓p = ↓(ninj p).
+// qed.
+
lemma npred_one: 𝟎 = ↓𝟏.
// qed.