proposition: Lemma char_poly : [char {poly R}] =i [char R].
proof: Proof. move=> p; rewrite !inE; congr (_ && _). apply/eqP/eqP=> [/(congr1 val) /=|]; last by rewrite -polyC_natr => ->. by rewrite polyseq0 -polyC_natr polyseqC; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)