proposition: Lemma real_nmono_in : {in D &, {homo f : x y /~ x < y}} -> {in [pred x in D | x \is real] &, {mono f : x y /~ x <= y}}.
proof: Proof. move=> Dmf x y /andP[hx xR] /andP[hy yR] /=. have [lt_xy|le_yx] := real_ltP xR yR; last by rewrite (ltW_nhomo_in Dmf). by rewrite lt_geF ?Dmf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)