proposition: Lemma morphpre_normal R S : R \subset f @* D -> S \subset f @* D -> (f @*^-1 R <| f @*^-1 S) = (R <| S).
proof: Proof. move=> sRfD sSfD; apply/idP/andP=> [|[sRS nSR]]. by move/morphim_normal; rewrite !morphpreK //; case/andP. by rewrite /(_ <| _) (subset_trans _ (morphpre_norm _)) morphpreS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)