fact: Record nneg_fun (T : Type) := mkNNFun { nneg_f :> T -> R ; nneg_f_ge0 : forall a, 0 <= nneg_f a }.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)