proposition: Lemma pred_absolu : forall x : Z, (0 < x)%Z -> pred (Z.abs_nat x) = Z.abs_nat (x - 1).
proof: Proof. intros x Hx. generalize (Z_lt_lt_S_eq_dec 0 x Hx); simpl in |- *; intros [H1| H1]; [ replace (Z.abs_nat x) with (Z.abs_nat (x - 1 + 1)); [ idtac | apply f_equal with Z; auto with zarith ]; rewrite absolu_plus; [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; lia | auto with zarith | intro; discriminate ] | rewrite <- H1; reflexivity ]. Qed.
imports: Coq(Lia)