proposition: Lemma reciprocal_idempotent p: p`_0 != 0 -> reciprocal_pol (reciprocal_pol p) = p.
proof: Proof. move=> h;rewrite - polyP {1}/reciprocal_pol (reciprocal_size h) => i. rewrite coef_poly /reciprocal_pol coef_poly. case: (ltnP i (size p)); last by move => /(nth_default 0). move => isp; rewrite - (subnKC isp). by rewrite -subn_gt0 addSn addnC -addnS addnK addKn addnS addnC -addnS addnK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)