proposition: Lemma qlogp_eq0 (q : qT) : (qlogp q == 0%N) = (q == 0) || (q == 1).
proof: Proof. case: (q =P 0) => [->|/eqP q_neq0]/=; first by rewrite qlogp0. case: (q =P 1) => [->|/eqP q_neq1]/=; first by rewrite qlogp1. rewrite /qlogp; case: pickP => [x|/(_ (Ordinal (qlogp_lt q)))] /=. by case: ((x : nat) =P 0%N) => // ->; rewrite expr0 eq_sym (negPf q_neq1). by rewrite qlogp_qX // eqxx. 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)