proposition: Lemma shift_polyD c1 c2 p: p \shift (c2 + c1) = (p\shift c1) \shift c2.
proof: Proof. by rewrite /shift_poly - comp_polyA - shift_polyD1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)