fact: Structure map := Map { iso_of_map : iso_map; _ : continuous iso_of_map }.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)