proposition: Lemma divgrMid x y : x \in K -> y \in H -> divgr K H (x * y) = x.
proof: Proof. by move=> Kx Hy; rewrite /divgr remgrMid ?mulgK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)