proposition: Theorem Z_to_nat_and_back : forall x:Z, (0 <= x)%Z -> (Z.of_nat (Z.abs_nat x))=x.
proof: Proof. intros x; case x. - reflexivity. - intros p Hd; elim p. + unfold Z.abs_nat; intros p' Hrec; rewrite nat_of_P_xI. rewrite inj_S, inj_mult, Zpos_xI. unfold Z.succ; rewrite Hrec; simpl; auto. + unfold Z.abs_nat; intros p' Hrec; rewrite nat_of_P_xO. rewrite inj_mult, Zpos_xO. unfold Z.succ; rewrite Hrec; simpl; auto. + simpl; auto. - intros p' Hd; elim Hd;auto. Qed.
imports: ZArith Arith Lia