proposition: Proposition diff_rank_quasi_cent_cycle m : (2 * \rank 'E_0 = 2 * \rank 'E_m + \sum_(i < h) `|'n_i - 'n_(i + m)| ^ 2)%N.
proof: Proof. rewrite !rank_quasi_cent_cycle !{1}mul2n -addnn. rewrite {1}(reindex (fun i : 'I_h => inh (i + m))) /=; last first. exists (fun i : 'I_h => inh (i + (h - m %% h))%N) => i _. apply: val_inj; rewrite /= modnDml -addnA addnCA -modnDml addnCA. by rewrite subnKC 1?ltnW ?ltn_mod // modnDr modn_small. apply: val_inj; rewrite /= modnDml -modnDmr -addnA. by rewrite subnK 1?ltnW ?ltn_mod // modnDr modn_small. rewrite -mul2n big_distrr -!big_split /=; apply: eq_bigr => i _. by rewrite !addn0 (addnC (2 * _)%N) sqrn_dist addnC /n_ Vi_mod. 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 gfunctor commutator gproduct) mathcomp(ssralg finalg zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)