proposition: Lemma horner_reciprocal1 p x : x \is a GRing.unit -> p.[x] = x ^+ (size p - 1) * (reciprocal_pol p).[x^-1].
proof: Proof. move=> xz; rewrite horner_reciprocal ?unitrV //. by rewrite mulrA invrK - exprMn divrr // expr1n mul1r. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)