proposition: Lemma Z_inj_nat_id: forall (z : Z), Z_inj_nat_rev (Z_inj_nat z) = z.
proof: Proof. intros z. unfold Z_inj_nat, Z_inj_nat_rev. destruct z eqn:Hdz. - reflexivity. - rewrite Pos2Nat.id. destruct (Pos.to_nat p~0) eqn:Hd. + pose proof Pos2Nat.is_pos p~0 as H. rewrite <- Nat.neq_0_lt_0 in H. exfalso; apply H, Hd. + reflexivity. - rewrite Pos2Nat.id. destruct (Pos.to_nat (Pos.pred_double p)) eqn: Hd. + pose proof Pos2Nat.is_pos (Pos.pred_double p) as H. rewrite <- Nat.neq_0_lt_0 in H. exfalso; apply H, Hd. + destruct (Pos.pred_double p) eqn:Hd2. * rewrite <- Pos.pred_double_succ in Hd2. apply Pos_pred_double_inj in Hd2. rewrite Hd2; reflexivity. * apply (f_equal Pos.succ) in Hd2. rewrite Pos.succ_pred_double in Hd2. rewrite <- Pos.xI_succ_xO in Hd2. inversion Hd2. * change xH with (Pos.pred_double xH) in Hd2. apply Pos_pred_double_inj in Hd2. rewrite Hd2; reflexivity. Qed.
imports: ZArith ConstructiveEpsilon