proposition: Lemma divgr_eq A B x : x = divgr A B x * remgr A B x.
proof: Proof. by rewrite mulgKV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)