proposition: Lemma segment_continuous_le_can_sym a b f g : a <= b -> {within `[a, b], continuous f} -> {in `[a, b], cancel f g} -> {in `[f a, f b], cancel g f}.
proof: Proof. move=> aLb fct fK x xfafb; apply: (segment_continuous_can_sym aLb fct fK). have : f a <= f b by rewrite (itvP xfafb). by case: ltrgtP xfafb => // ->. 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)