proposition: Lemma mem_dprod G A B x : A \x 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. move=> defG; have [_ _ cBA _] := dprodP defG. by apply: mem_sdprod; rewrite -dprodEsd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)