proposition: Lemma posnumeP (R : numDomainType) (x : \bar R) : 0 < x -> posnume_spec x x (x == 0) (0 <= x) (0 < x).
proof: Proof. case: x => [x|_|//]; last by rewrite le0y lt0y; exact: IsPinftyPosnume. rewrite lte_fin lee_fin eqe => x_gt0. rewrite x_gt0 (ltW x_gt0) (negbTE (lt0r_neq0 x_gt0)). exact: IsRealPosnume (PosNum x_gt0). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed