proposition: Lemma pcan_in_inj [rT aT : Type] [A : {pred aT}] [f : aT -> rT] [g : rT -> option aT] : {in A, pcancel f g} -> {in A &, injective f}.
proof: Proof. by move=> fK x y Ax Ay /(congr1 g); rewrite !fK// => -[]. Qed.
imports: ssreflect ssrfun