proposition: Lemma absolu_pred_nat : forall (m : Z) (Hm : (0 < m)%Z), S (pred_nat m Hm) = Z.abs_nat m.
proof: Proof. intros [| px| px] Hx; try discriminate Hx. unfold pred_nat in |- *. rewrite S_predn. reflexivity. apply pred_nat_unfolded_subproof. Qed.
imports: Coq(Lia)