proposition: Lemma nat_of_P_nonzero (p: positive): nat_of_P p <> 0.
proof: Proof. intro H. apply Nat.lt_irrefl with 0. rewrite <- H at 2. apply lt_O_nat_of_P. Qed.
imports: Coq.Setoids.Setoid Coq.PArith.BinPos Coq.PArith.Pnat ZArith_base