proposition: Lemma translate_polq {R : comRingType} (l : {poly R}) a x : (translate_pol l a).[x] = l.[x + a].
proof: Proof. by rewrite /translate_pol horner_comp 3!hornerE. Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc