proposition: Lemma morphimI A B : f @* (A :&: B) \subset f @* A :&: f @* B.
proof: Proof. by rewrite subsetI // ?morphimS ?(subsetIl, subsetIr). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)