proposition: Lemma card_GFqm : #| GF | = q ^ m.
proof: Proof. rewrite /GF; by case: (@PrimePowerField q m primeq isT). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2 mathcomp(finfield)