proposition: Theorem inj_abs : forall x : Z, (0 <= x)%Z -> Z_of_nat (Z.abs_nat x) = x.
proof: Proof. intros x; elim x; auto. unfold Z.abs_nat in |- *. intros p. pattern p at 1 3 in |- *; rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id p). generalize (convert_not_O p); case (nat_of_P p); simpl in |- *; auto with arith. intros H'; case H'; auto. intros n H' H'0; rewrite Pos.pred_succ; auto. intros p H'; contradict H'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz