proposition: Lemma poly_comp_exp (p r: {poly R}) i: (p ^+i) \Po r = (p \Po r) ^+ i.
proof: Proof. elim: i => [| i ihi]; first by rewrite !expr0 comp_polyC. by rewrite !exprS comp_polyM ihi. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)