proposition: Lemma reciprocal_Xn (R : idomainType) n : reciprocal_pol ('X^n) = (GRing.one R)%:P.
proof: Proof. rewrite /reciprocal_pol size_polyXn poly_def big_ord_recl. rewrite subSS subn0 coefXn expr0 eqxx scale1r big1 ?addr0 // => i _. rewrite lift0 subSS coefXn /=. have /negbTE -> : (n - i.+1)%N != n. by rewrite neq_ltn -(ltn_add2r i.+1) subnK// -addSnnS ltn_addr. by rewrite -mul_polyC mul0r. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)