proposition: Lemma recip0 : recip deg (0 :{poly R}) = 0.
proof: Proof. rewrite recipE; last by rewrite size_poly0. by rewrite poly_def; apply: big1 => i _; rewrite polyseq0 nth_nil scale0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc