proposition: Lemma morphim_coprime_sdprod : K ><| H = G -> coprime #|K| #|H| -> f @* K ><| f @* H = f @* G.
proof: Proof. rewrite /sdprod => defG coHK; move: defG. by rewrite !coprime_TIg ?coprime_morph // !subxx; apply: morphim_pprod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)