proposition: Proposition rank_eigenspaces_free_quasi_homocyclic : q > 1 -> 'n_0 = 0%N -> h = q.+1 /\ (forall j, j != 0 %[mod h] -> 'n_j = 1%N).
proof: Proof. move=> q_gt1 n_0; rewrite mod0n. have [n d_q_hn [i [n_i lt_q_hn n_i']]] := rank_eigenspaces_quasi_homocyclic. move/eqP: d_q_hn; rewrite distn_eq1 {}lt_q_hn. case: (eqVneq (Ordinal h_gt0) i) n_i n_i' => [<- | ne0i _ n_i']; last first. by rewrite -(n_i' _ ne0i) n_0 /= muln0 -(subnKC q_gt1). rewrite n_0 dist0n => -> n_i'; rewrite muln1 => /eqP->; split=> // i'. by move/(n_i' (inh i')); rewrite /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)