proposition: Theorem NconvertO : forall p : positive, nat_of_P p <> 0.
proof: Proof. intros p; elim p; unfold nat_of_P in |- *; simpl in |- *. intros p0 H'; red in |- *; intros H'0; discriminate. intros p0; rewrite ZL6; unfold nat_of_P in |- *. case (Pmult_nat p0 1); simpl in |- *; auto. red in |- *; intros H'; discriminate. Qed.
imports: Reals ZArith List PeanoNat Psatz