proposition: Lemma pcontinuous_is_hereditary : pcontinuous -> hereditary.
proof: Proof. move=> Fcont gT H G sHG; rewrite -{2}(setIidPl sHG) setIC. by do 2!rewrite -(morphim_idm (subsetIl H _)) morphimIdom ?Fcont. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)