proposition: Lemma comp_polyXsub1 n : ('X - 1) \Po 'X^n = 'X^n - 1 :> {poly R}.
proof: Proof. by rewrite comp_polyB comp_polyC comp_polyX. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)