proposition: Theorem Pos2Nat_to_pos : ∀ x, (0 < x)%Z → Pos.to_nat (Z.to_pos x) = Z.to_nat x.
proof: Proof. intros x Hx. destruct x as [| x| x]. exfalso; revert Hx; apply Z.lt_irrefl. reflexivity. exfalso; apply Z.nle_gt in Hx. apply Hx, Pos2Z.neg_is_nonpos. Qed.
imports: Utf8 QArith NPeano Sorted Psatz