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