fact: Definition qlogp (p : qT) : nat := odflt (Ordinal pred_card_qT_gt0) (pick [pred i in 'I_ _ | ('qX ^+ i == p)]).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(div bigop binomial finset finfun ssralg countalg finalg) mathcomp(poly polydiv qpoly perm fingroup falgebra fieldext finfield galois) mathcomp(finalg zmodp matrix vector)