proposition: Lemma injm_sdprodm : 'injm sdprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == 1].
proof: Proof. rewrite ker_sdprodm -(ker_pprodm sdprodm_norm actf sdprodm_eqf) injm_pprodm. congr [&& _, _ & _ == _]; have [_ _ _ tiHK] := sdprodP eqHK_G. by rewrite -morphimIdom tiHK morphim1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)