proposition: Lemma sdprod_recr n G K H H1 : #|G| <= n -> K ><| H = G -> H1 \proper H -> exists G1 : {group gT}, [/\ #|G1| < n, G1 \subset G & K ><| H1 = G1].
proof: Proof. move=> leGn; case/sdprodP=> _ defG nKH tiKH ltH1H. have [sH1H _] := andP ltH1H; have nKH1 := subset_trans sH1H nKH. have tiKH1: K :&: H1 = 1 by apply/trivgP; rewrite -tiKH setIS. exists (K <*> H1)%G; rewrite /= -defG sdprodE // norm_joinEr //. rewrite ?mulgS // ?(leq_trans _ leGn) //=. by rewrite -defG ?TI_cardMg // ltn_pmul2l ?proper_card. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)