proposition: Lemma isnat_abs_inj : forall (x : Z) (n : nat), (0 <= x)%Z -> n = Z.abs_nat x -> x = Z_of_nat n.
proof: Proof. intros. rewrite H0. rewrite inj_abs_pos. reflexivity. apply Z.le_ge. assumption. Qed.
imports: ZArith EqNat lemmas