proposition: Lemma shift_polyDK c p: p \shift c \shift -c = p.
proof: Proof. by rewrite - shift_polyD addrC subrr /shift_poly addr0 comp_polyXr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)