proposition: Lemma inj_abs_nat z : Z.of_nat (Z.abs_nat z) = Z.abs z.
proof: Proof. destruct z as [|p|p]; simpl; trivial; destruct (Pos2Nat.is_succ p) as (n,H); rewrite H; simpl; f_equal; now apply SuccNat2Pos.inv. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat