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