proposition: Lemma recipD : forall q1 q2 : {poly R}, (size q1 <= deg.+1)%N -> (size q2 <= deg.+1)%N -> recip deg (q1 + q2) = recip deg q1 + recip deg q2.
proof: Proof. move=> q1 q2 s1 s2; rewrite !recipE // ?poly_def; last first. by rewrite (leq_trans (size_add _ _)) // geq_max s1 s2. have t : forall i : 'I_deg.+1, true -> (q1 + q2)`_(deg.+1 - i.+1) *: 'X^i = q1`_(deg.+1 - i.+1) *: 'X^i + q2`_(deg.+1 - i.+1) *: 'X^i. by move=> [i ci] _ /=; rewrite coef_add_poly scalerDl. by rewrite (eq_bigr _ t) big_split. 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