proposition: Lemma mono_surj_image_segment a b f : a <= b -> monotonous `[a, b] f -> set_surj `[a, b] (f @`[a, b]) f -> f @` `[a, b] = f @`[a, b]%classic.
proof: Proof. move=> leab fmono; apply: surj_image_eq => _ /= [x xab <-]; exact: mono_mem_image_segment. 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