proposition: Lemma horner_shift_poly1 c p x : p.[x] = (p \shift c).[x - c].
proof: Proof. by rewrite horner_shift_poly addrNK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)