proposition: Lemma quotient_pprod : pprod K H = G -> pprod (K / M) (H / M) = G / M.
proof: Proof. exact: morphim_pprod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)