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