proposition: Lemma homo_mono1 [aT rT : Type] [f : aT -> rT] [g : rT -> aT] [aP : pred aT] [rP : pred rT] : cancel g f -> {homo f : x / aP x >-> rP x} -> {homo g : x / rP x >-> aP x} -> {mono g : x / rP x >-> aP x}.
proof: Proof. by move=> gK fP gP x; apply/idP/idP => [/fP|/gP//]; rewrite gK. Qed.
imports: mathcomp(ssreflect ssrfun)