proposition: Lemma sdprod_recl n G K H K1 : #|G| <= n -> K ><| H = G -> K1 \proper K -> H \subset 'N(K1) -> exists G1 : {group gT}, [/\ #|G1| < n, G1 \subset G & K1 ><| H = G1].
proof: Proof. move=> leGn; case/sdprodP=> _ defG nKH tiKH ltK1K nK1H. have tiK1H: K1 :&: H = 1 by apply/trivgP; rewrite -tiKH setSI ?proper_sub. exists (K1 <*> H)%G; rewrite /= -defG sdprodE // norm_joinEr //. rewrite ?mulSg ?proper_sub ?(leq_trans _ leGn) //=. by rewrite -defG ?TI_cardMg // ltn_pmul2r ?proper_card. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)