proposition: Lemma qlogp0 : qlogp 0 = 0%N.
proof: Proof. rewrite /qlogp; case: pickP => //= x. by rewrite (expf_eq0 ('qX : qT)) (negPf qX_neq0) andbF. 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)