proposition: Lemma isog_dprod A B G C D L : A \x B = G -> C \x D = L -> isog A C -> isog B D -> isog G L.
proof: Proof. move=> defG {C D} /dprodP[[C D -> ->] defL cCD trCD]. case/dprodP: defG (defG) => {A B} [[A B -> ->] defG _ _] dG defC defD. case/isogP: defC defL cCD trCD => fA injfA <-{C}. case/isogP: defD => fB injfB <-{D} defL cCD trCD. apply/isogP; exists (dprodm_morphism dG cCD). by rewrite injm_dprodm injfA injfB trCD eqxx. by rewrite /= -{2}defG morphim_dprodm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)