proposition: Lemma segment_can_continuous a b f g : a <= b -> {within `[a, b], continuous f} -> {in `[a, b], cancel f g} -> {within f @`[a, b], continuous g}.
proof: Proof. move=> aLb crf fK x; case: lerP => // _; by [apply: segment_can_ge_continuous|apply: segment_can_le_continuous]. 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)