proposition: Theorem absolu_lt_nz : forall z : Z, z <> 0%Z -> 0 < Z.abs_nat z.
proof: Proof. intros z; case z; simpl in |- *; auto; try (intros H'; case H'; auto; fail); intros p; generalize (NconvertO p); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz