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. - auto. - intros p Hd; elim p. + unfold Z.abs_nat; intros p' Hrec; rewrite nat_of_P_xI. rewrite inj_S. rewrite inj_mult. rewrite Zpos_xI. unfold Z.succ. rewrite Hrec. simpl; auto. + unfold Z.abs_nat. intros p' Hrec; rewrite nat_of_P_xO. rewrite inj_mult. rewrite Zpos_xO. unfold Z.succ. rewrite Hrec. simpl; auto. + simpl; auto. - intros p' Hd; elim Hd;auto. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv