proposition: Lemma sdpairE (u : sdT) : u = sdpair2 u.1 * sdpair1 u.2.
proof: Proof. apply: val_inj; case: u => [[a x] /= /setXP[Da Rx]]. by rewrite !val_insubd !inE Da Rx !(group1, gact1) // mulg1 mul1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)