proposition: Lemma morphpreSK R S : R \subset f @* D -> (f @*^-1 R \subset f @*^-1 S) = (R \subset S).
proof: Proof. move=> sRfD; apply/idP/idP=> [sf'RS|]; last exact: morphpreS. suffices: R \subset f @* D :&: S by rewrite subsetI sRfD. rewrite -(morphpreK sRfD) -[_ :&: S]morphpreK (morphimS, subsetIl) //. by rewrite morphpreI morphimGK ?subsetIl // setIA setIid. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)