proposition: Lemma inj_can_sym_in : {homo f \o g : x / x \in rD} -> {on rD, cancel f & g} -> {in rD &, injective g} -> {in rD, cancel g f}.
proof: Proof. by move=> fgD fK gI x x_rD; apply: gI; rewrite ?fK ?fgD. Qed.
imports: ssreflect ssrfun