proposition: Lemma logn_card_GL_p n p : prime p -> logn p #|'GL_n(p)| = 'C(n, 2).
proof: Proof. move=> p_pr; have p_gt1 := prime_gt1 p_pr. have p_i_gt0: p ^ _ > 0 by move=> i; rewrite expn_gt0 ltnW. have <- : #|'GL_n.-1.+1(p)| = #|'GL_n(p)| by []. rewrite (card_GL _ (ltn0Sn n.-1)) card_ord Fp_cast // big_add1 /=. pose p'gt0 m := m > 0 /\ logn p m = 0. suffices [Pgt0 p'P]: p'gt0 (\prod_(0 <= i < n.-1.+1) (p ^ i.+1 - 1))%N. by rewrite lognM // p'P pfactorK // addn0; case n. apply: big_ind => [|m1 m2 [m10 p'm1] [m20]|i _]; rewrite {}/p'gt0 ?logn1 //. by rewrite muln_gt0 m10 lognM ?p'm1. rewrite lognE -if_neg subn_gt0 p_pr /= -{1 2}(exp1n i.+1) ltn_exp2r // p_gt1. by rewrite dvdn_subr ?dvdn_exp // gtnNdvd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)