proposition: Lemma reciprocal_nth_2 (p : {poly R}) k : (k < size p)%N -> (reciprocal_pol p)`_(size p - k.+1) = p`_k.
proof: Proof. move=> Hk. rewrite /reciprocal_pol coef_poly. have Hk2 : (size p - k.+1 < size p)%N. by rewrite -(ltn_add2r k.+1) subnK // -addSnnS ltn_addr. rewrite Hk2 !subnS -!subn1 !subnBA; last by rewrite subn_gt0. by rewrite addn1 -subnDA addn1 addnC addnK. exact: ltnW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)