proposition: Lemma quotient_sdprodr_isog G A B M : A ><| B = G -> M <| B -> B / M \isog G / (A <*> M).
proof: Proof. move=> defG; case/sdprodP: defG (defG) => [[K H -> ->] _ _ _] => defG nsMH. by have [h /isom_isog->] := quotient_sdprodr_isom defG nsMH. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)