proposition: Lemma mono_mem_image_itvoo a b f : monotonous `[a, b] f -> {homo f : x / x \in `]a, b[ >-> x \in f @`]a, b[}.
proof: Proof. move=> []/[dup] => [/leW_mono_in|/leW_nmono_in] flt fle x xab; have ltab : a < b by rewrite (itvP xab). have: f a <= f b by rewrite ?fle ?bound_itvE ?ltW. by case: leP => // fafb _; rewrite in_itv/= ?flt ?in_itv/= ?(itvP xab, lexx). have: f a >= f b by rewrite fle ?bound_itvE ?ltW. by case: leP => // fafb _; rewrite in_itv/= ?flt ?in_itv/= ?(itvP xab, lexx). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule