proposition: Lemma nonnegeP (R : numDomainType) (x : \bar R) : 0 <= x -> nonnege_spec x x (0 <= x).
proof: Proof. case: x => [x|_|//]; last by rewrite le0y; exact: IsPinftyNonnege. by rewrite lee_fin => /[dup] x_ge0 ->; exact: IsRealNonnege (NngNum x_ge0). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed