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