(* 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_one: 𝟎 = ↓𝟏.
+lemma npred_inj (p): ↓p = ↓(ninj p).
+// qed.
+
+lemma npred_unit: 𝟎 = ↓𝟏.
// qed.
lemma npred_psucc (p): ninj p = ↓↑p.
lemma npred_pnat_inv_refl (p): ninj p = ↓p → ⊥.
*
-[ <npred_one #H destruct
+[ <npred_unit #H destruct
| #p /3 width=2 by psucc_inv_refl, eq_inv_ninj_bi/
]
qed-.