proposition: Lemma mem_dec_segment d (T : porderType d) (a b : T) (f : T -> T) : {in `[a, b] &, {mono f : x y /~ (x <= y)%O}} -> {homo f : x / x \in `[a, b] >-> x \in `[f b, f a]}.
proof: Proof. move=> fge x xab; have leab : (a <= b)%O by rewrite (itvP xab). by rewrite in_itv/= !fge ?(itvP xab). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed