(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
-(* Rewrites with nsucc ******************************************************)
+(* Constructions with nsucc *************************************************)
-(*** pred_Sn *)
+(*** pred_Sn pred_S *)
lemma npred_succ (n): n = ↓↑n.
* //
qed.