proposition: Lemma Z_to_nat_to_Z_i : forall (n:nat), Z_to_nat_i (nat_to_Z_i n) = n.
proof: Proof. intros [|n]; unfold nat_to_Z_i. case (even_odd_exists_dec 0); intros [k Hk]; transitivity (Z_to_nat_i (Z_of_nat 0)); trivial; apply (f_equal Z_to_nat_i); simpl; unfold Nat.double in Hk; lia. case (even_odd_exists_dec (S n)); intros [[|k] Hk]; rewrite Hk; trivial; simpl; [apply (f_equal Nat.double); apply nat_of_P_o_P_of_succ_nat_eq_succ |transitivity (pred (Nat.double (S k))); trivial; apply (f_equal pred); apply (f_equal Nat.double); apply nat_of_P_o_P_of_succ_nat_eq_succ ]. Defined.
imports: Coq(ZArith) Coq(Lia)