proposition: Lemma shift_polyB1 (c1 c2 : R): (c1%:P - 'X) \shift c2 = (c1 - c2)%:P -'X.
proof: Proof. rewrite /shift_poly comp_polyB comp_polyC comp_polyX opprD. by rewrite - addrCA addrC polyCB. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)