proposition: Lemma nonnegP (R : numDomainType) (x : R) : 0 <= x -> nonneg_spec x x (0 <= x).
proof: Proof. by move=> xge0; rewrite xge0 -[x]/(NngNum xge0)%:num; constructor. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)