proposition: Lemma nat_to_Z_to_nat_i : forall (z:Z), nat_to_Z_i (Z_to_nat_i z) = z.
proof: Proof. intros [|p|p]; unfold nat_to_Z_i. simpl; case (even_odd_exists_dec 0); intros [k Hk]; [transitivity (Z_of_nat 0) |transitivity (Z.opp (Z_of_nat 0)) ]; trivial; try apply (f_equal Z.opp); apply (f_equal Z_of_nat); unfold Nat.double in Hk; lia. case (even_odd_exists_dec (Z_to_nat_i (Zpos p)) ); intros [k Hk]. unfold Z_to_nat_i in Hk; rewrite <- (double_eq_half_eq _ _ Hk); symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P. apply False_ind; unfold Z_to_nat_i in Hk; destruct (ZL4 p) as [m Hm]; rewrite Hm in Hk; apply (double_S_neq_pred m k); assumption. case (even_odd_exists_dec (Z_to_nat_i (Zneg p)) ); intros [k Hk]. unfold Z_to_nat_i in Hk; unfold Nat.double in Hk; destruct (ZL4 p) as [m Hm]; lia. unfold Z_to_nat_i in Hk; case (eq_add_pred _ _ Hk). intro Hk'; rewrite <- (double_eq_half_eq _ _ Hk'); symmetry; apply Z.opp_inj; rewrite Zopp_neg; rewrite Z.opp_involutive; apply Zpos_eq_Z_of_nat_o_nat_of_P. intros [H_nat_p_lt_2 _]; apply False_ind; destruct (ZL4 p) as [m Hm]; rewrite Hm in H_nat_p_lt_2; unfold Nat.double in H_nat_p_lt_2; rewrite Nat.add_succ_r in H_nat_p_lt_2; lia. Defined.
imports: Coq(ZArith) Coq(Lia)