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