proposition: Lemma pprodmE x a : x \in H -> a \in K -> f (x * a) = fH x * fK a.
proof: Proof. move=> Hx Ka; have: x * a \in H * K by rewrite mem_mulg. rewrite -remgrP inE /f rcoset_sym mem_rcoset /divgr -mulgA groupMl //. case/andP; move: (remgr H K _) => b Hab Kb; rewrite morphM // -mulgA. have Kab: a * b^-1 \in K by rewrite groupM ?groupV. by congr (_ * _); rewrite eqfHK 1?inE ?Hab // -morphM // mulgKV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)