proposition: Lemma mem_sdprod G A B x : A ><| B = G -> x \in G -> exists y, exists z, [/\ y \in A, z \in B, x = y * z & {in A & B, forall u t, x = u * t -> u = y /\ t = z}].
proof: Proof. case/sdprodP=> [[K H -> ->{A B}] <- _ tiKH] /mulsgP[y z Ky Hz ->{x}]. exists y; exists z; split=> // u t Ku Ht eqyzut. move: (congr1 (divgr K H) eqyzut) (congr1 (remgr K H) eqyzut). by rewrite !remgrMid // !divgrMid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)