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