proposition: Lemma segment_can_mono a b f g : a <= b -> {within `[a, b], continuous f} -> {in `[a, b], cancel f g} -> monotonous (f @`[a, b]) g.
proof: Proof. move=> le_ab fct fK; rewrite /monotonous/=; case: ltrgtP => fab; [left|right..]; do ?by [apply: segment_can_le|apply: segment_can_ge]. by move=> x y /itvxxP<- /itvxxP<-; rewrite !lexx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)