proposition: Lemma shift_polyD1 (c1 c2 : R): ('X + c1%:P) \shift c2 = ('X + (c2 + c1)%:P).
proof: Proof. by rewrite /shift_poly comp_polyD comp_polyX comp_polyC polyCD addrA. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)