proposition: Lemma reciprocalM p q : reciprocal_pol (p * q) = reciprocal_pol p * reciprocal_pol q.
proof: Proof. move: (reciprocalC (GRing.zero R)) => aux. case (poly0Vpos p); first by move => ->; rewrite mul0r aux mul0r. case (poly0Vpos q); first by move => -> _; rewrite mulr0 aux mulr0. set m:= (size p + size q).-1; move=> pa pb. have mp: (size p + size q)%N = m .+1. by symmetry;rewrite /m prednK // addn_gt0 pa pb. have qa: (size p <= m)%N by rewrite /m - (prednK pa) addnS leq_addr. have qb: (size q <= m)%N by rewrite /m addnC - (prednK pb) addnS leq_addr. have pnz: p != 0 by rewrite - size_poly_eq0 - lt0n. have qnz: q != 0 by rewrite - size_poly_eq0 - lt0n. rewrite /reciprocal_pol size_mul //. rewrite - polyP => i; rewrite coef_poly coefM coefM. case: (ltnP i (size p + size q).-1) => ipq; last first. rewrite big1 // => [] [] j ij _ /=; rewrite ! coef_poly. case lt1: (j < size p)%N; last by rewrite mul0r. case lt2: (i - j < size q)%N; last by rewrite mulr0. move: (leq_add lt1 lt2). by rewrite addnS addSn mp ltnS subnKC ? ltnS // ltnNge ipq. set mi:= ((size p + size q).-1 - i.+1)%N. pose f j := (p`_j * q`_(mi - j)). have aux1: forall j, (size p <=j) %N -> f j = 0. by move=> j; rewrite /f; move => /(nth_default 0) => ->; rewrite mul0r. rewrite (bigop_simpl1 _ mi.+1 aux1). pose g1 j := (\poly_(i0 < size p) p`_(size p - i0.+1))`_j. pose g2 j := (\poly_(i0 < size q) q`_(size q - i0.+1))`_j. pose g j := g1 j * g2 (i - j)%N. have aux2: forall j : nat, (size p <= j)%N -> g j = 0. by move => j; rewrite /g/g1 coef_poly ltnNge; move => ->; rewrite mul0r. rewrite (bigop_simpl1 _ i.+1 aux2). transitivity (\sum_(j < size p | (j < i.+1)%N) p`_(size p - j.+1) * g2 (i - j)%N); last first. by apply: eq_big => // [[j ji]] _ /=; rewrite /g/g1 coef_poly ji. symmetry; rewrite (big_ord_rev _ (size p) (fun j => (j < i.+1)%N) (fun j => p`_(size p - j.+1) * g2 (i - j)%N)) /=. rewrite big_mkcond [X in _ = X] big_mkcond; apply: eq_bigr => [[k kp]] _ /=. case Ha: ((size p - k.+1) < i.+1)%N; last first. case Hb: (k < mi.+1)%N => //; rewrite /f. suff:(size q <= (mi - k))%N by move => /(nth_default 0) => ->; rewrite mulr0. rewrite ltnS in Hb; rewrite -(leq_add2l k) (subnKC Hb) -(leq_add2l i.+1). rewrite (subnKC ipq) addSn addnA -ltnS mp /= -mp -addSn -addSn leq_add2r. by rewrite -addnS -(subnK kp) -addSn leq_add2r ltnNge -ltnS Ha. rewrite (subnSK kp) (subKn (ltnW kp)) (subnBA _ kp) - addSnnS. move: Ha; rewrite ltnS leq_subLR addSnnS addnC => Ha. have ->: (k < mi.+1)%N = (i.+1 + k <= m)%N. by rewrite /mi ltnS - (leq_add2l (i.+1)) (subnKC ipq) mp. rewrite /g2 coef_poly; case Hb: (i.+1 + k <= m)%N; last first. suff: ~~(i.+1 + k - size p < size q)%N by move /negbTE => ->;rewrite mulr0. by rewrite -ltnNge ltnS - (leq_add2l (size p)) (subnKC Ha) mp ltnNge Hb. rewrite /f - (ltn_add2l (size p)) (subnKC Ha) mp ltnS Hb; congr (_ * (q`_ _)). apply /eqP; rewrite - (eqn_add2r (i.+1 + k)%N)- subnDA (subnK Hb). have m1: m = (size p + (size q).-1)%N by rewrite /m -(ltn_predK pa) addnS. rewrite addnC -(ltn_predK pa) subSS - {1} (subnK Ha) (addnC _ (size p)). by rewrite - addnA m1 subnKC // leq_subLR - m1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)