proposition: Lemma horner_reciprocal p x : x \is a GRing.unit -> (reciprocal_pol p).[x] = x ^+ (size p - 1) * p.[x^-1].
proof: Proof. move=> xn0; rewrite /reciprocal_pol horner_poly. case sp : (size p) => [| n]. rewrite sub0n expr0 mul1r big_ord0; move/eqP: sp; rewrite size_poly_eq0. by move/eqP->; rewrite horner0. rewrite horner_coef subn1 /= big_distrr /=. pose f (j : 'I_n.+1) := Ordinal (leq_subr j n:n - j < n.+1)%N. have finv: forall j:'I_n.+1, xpredT j -> f (f j) = j. by move => j _; apply: val_inj => /=; rewrite subKn //; have : (j < n.+1)%N. rewrite (reindex_onto f f finv) /=. have tmp :(fun j => f (f j) == j) =1 xpredT. by move=> j /=; apply/eqP; apply finv. rewrite (eq_bigl _ _ tmp) {tmp} sp; apply: eq_bigr => [[j hj]] _ /=. rewrite subSS subKn // -mulrCA; congr (_ * _). rewrite ltnS in hj; rewrite - {2}(subnK hj) exprD -mulrA exprVn. by rewrite divrr ? mulr1 // unitrX. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)