proposition: Fact Puig_at_cont n : GFunctor.iso_continuous (Puig_at n).
proof: Proof. elim: n => [|n IHn] aT rT G f injf; first by rewrite morphim1. have IHnS := Puig_at_sub n; pose func_n := [igFun by IHnS & !IHn]. rewrite !PuigS sub_morphim_pre ?Puig_succ_sub // gen_subG; apply/bigcupsP=> A. rewrite inE => /and3P[sAG nAL cAA]; rewrite -sub_morphim_pre ?sub_gen //. rewrite -[f @* A]/(gval _) bigcup_sup // inE morphimS // /norm_abelian. rewrite morphim_abelian // -['L_{n}(_)](injmF func_n injf) //=. by rewrite morphim_norms. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)