proposition: Lemma continuous_is_iso_continuous : continuous -> iso_continuous.
proof: Proof. by move=> Fcont gT hT G phi inj_phi; apply: Fcont. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)