proposition: Lemma qlogp1 : qlogp 1 = 0%N.
proof: Proof. case: (qlogp 1 =P 0%N) => // /eqP log1_neq0. have := qlogp_lt 1; rewrite ltnNge => /negP[]. apply: dvdn_leq; first by rewrite lt0n. by rewrite qX_order_dvd // qlogp_qX ?oner_eq0. Qed.
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)