proposition: Lemma sdprod_subr G A B M : A ><| B = G -> M \subset B -> A ><| M = A <*> M.
proof: Proof. case/sdprodP=> [[K H -> ->] _ nKH tiKH] sMH. by rewrite sdprodEY ?(subset_trans sMH) //; apply/trivgP; rewrite -tiKH setIS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)