proposition: Lemma can_in_pcan [rT aT : Type] (A : {pred aT}) [f : aT -> rT] [g : rT -> aT] : {in A, cancel f g} -> {in A, pcancel f (fun y : rT => Some (g y))}.
proof: Proof. by move=> fK x Ax; rewrite fK. Qed.
imports: ssreflect ssrfun