proposition: Lemma pred_nat_unfolded : forall (x : Z) (Hx : (0 < x)%Z), x = S (pred_nat x Hx).
proof: Proof. intros [| px| px] Hx; try discriminate Hx. unfold pred_nat in |- *. rewrite S_predn. symmetry in |- *; apply ZL9. clear Hx; apply pred_nat_unfolded_subproof. Qed.
imports: Coq(Lia)