proposition: Lemma posnumP (R : numDomainType) (x : R) : 0 < x -> posnum_spec x x (x == 0) (0 <= x) (0 < x).
proof: Proof. move=> x_gt0; case: real_ltgt0P (x_gt0) => []; rewrite ?gtr0_real // => _ _. by rewrite -[x]/(PosNum x_gt0)%:num; constructor. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(algC)