proposition: Lemma sdpair_act : {in R & D, forall x a, sdpair1 (to x a) = sdpair1 x ^ sdpair2 a}.
proof: Proof. move=> x a Rx Da; apply: val_inj. rewrite /= !val_insubd !inE !group1 gact_stable ?Da ?Rx //=. by rewrite !mul1g mulVg invg1 mulg1 actKVin ?mul1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)