proposition: Lemma qX_exp_neq0 i : 'qX ^+ i != 0 :> qT.
proof: Proof. by rewrite expf_eq0 negb_and qX_neq0 orbT. 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)