proposition: Lemma sdprod_mul1g : left_id sdprod_one sdprod_mul.
proof: Proof. move=> u; apply: val_inj; case: u => [[a x] /=]; case/setXP=> Da _. by rewrite gact1 // !mul1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)