proposition: Lemma segment_continuous_can_sym a b f g : a <= b -> {within `[a, b], continuous f} -> {in `[a, b], cancel f g} -> {in f @`[a, b], cancel g f}.
proof: Proof. move=> aLb ctf fK; have g_mono := segment_can_mono aLb ctf fK. have f_mono := itv_continuous_inj_mono ctf (can_in_inj fK). have f_surj := segment_continuous_surjective aLb ctf. have fIP := mono_surj_image_segmentP aLb f_mono f_surj. suff: {in f @`[a, b], {on `[a, b], cancel g & f}}. by move=> gK _ /fIP[x xab <-]; rewrite fK. have: {in f @`[a, b] &, {on `[a, b] &, injective g}}. by move=> _ _ /fIP [x xab <-] /fIP[y yab <-]; rewrite !fK// => _ _ ->. by apply/ssrbool.inj_can_sym_in_on => x xab; rewrite ?fK ?mono_mem_image_segment. 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)