proposition: Lemma abs_inj : forall n : nat, Z.abs_nat (Z_of_nat n) = n.
proof: Proof. simple induction n. simpl in |- *. reflexivity. intros m IH. rewrite <- IH. simpl in |- *. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. reflexivity. Qed.
imports: ZArith EqNat lemmas