proposition: Lemma introspec_char (F : finFieldType) (k p c : nat) : p \in [char F] -> p ⋈[k] ('X + c%:R%:P : {poly F}).
proof: Proof. move=> pC; apply/eqP; congr (rmodp _ _). have Pp : prime p by apply: charf_prime pC. have Cn : [char F].-nat p by rewrite pnatE. rewrite comp_polyD comp_polyC comp_polyX. rewrite exprDn_char; first by rewrite -polyC_exp fin_little_fermat. by rewrite pnatE // (rmorph_char (GRing.RMorphism.clone _ _ _ polyC)). Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound