proposition: Lemma injmI A B : f @* (A :&: B) = f @* A :&: f @* B.
proof: Proof. rewrite -morphimIdom setIIr -4!(injmK (subsetIl D _), =^~ morphimIdom). by rewrite -morphpreI morphpreK // subIset ?morphim_sub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)