proposition: Lemma morphpreI R S : f @*^-1 (R :&: S) = f @*^-1 R :&: f @*^-1 S.
proof: Proof. by rewrite -setIIr -preimsetI. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)