proposition: Theorem Zposnat2Znat : ∀ i, (0 < i)%nat → Zpos (Pos.of_nat i) = Z.of_nat i.
proof: Proof. intros i Hi. destruct i; [ apply lt_irrefl in Hi; contradiction | clear Hi ]. simpl; f_equal. induction i; [ reflexivity | simpl ]. rewrite IHi; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz