proposition: Lemma char_qpoly : [char {poly %/ h}] =i [char A].
proof: Proof. move=> p; rewrite !inE; congr (_ && _). apply/eqP/eqP=> [/(congr1 val) /=|pE]; last first. by apply: val_inj => //=; rewrite qpolyC_natr /= -polyC_natr pE. rewrite !qpolyC_natr -!polyC_natr => /(congr1 val) /=. by rewrite polyseqC polyseq0; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun ssralg countalg finalg poly polydiv) mathcomp(perm fingroup matrix mxalgebra mxpoly vector countalg)