fact: Definition partial_product A B := if A == 1 then B else if B == 1 then A else if [&& group_set A, group_set B & B \subset 'N(A)] then A * B else set0.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)