proposition: Lemma comm_redivpP m d : comm_redivp_spec m d (redivp m d).
proof: Proof. rewrite unlock; have [->|Hd] := eqVneq d 0. by constructor; rewrite !(simp, eqxx). have: GRing.comm d (lead_coef d)%:P -> m * (lead_coef d ^+ 0)%:P = 0 * d + m. by rewrite !simp. elim: (size m) 0%N 0 {1 4 6}m (leqnn (size m)) => [|n IHn] k q r Hr /=. move/size_poly_leq0P: Hr ->. suff hsd: size (0: {poly R}) < size d by rewrite hsd => /= ?; constructor. by rewrite size_poly0 size_poly_gt0. case: ltnP => Hlt Heq; first by constructor. apply/IHn=> [|Cda]; last first. rewrite mulrDl addrAC -addrA subrK exprSr polyCM mulrA Heq //. by rewrite mulrDl -mulrA Cda mulrA. apply/leq_sizeP => j Hj; rewrite coefB coefMC -scalerAl coefZ coefXnM. rewrite ltn_subRL ltnNge (leq_trans Hr) /=; last first. by apply: leq_ltn_trans Hj _; rewrite -add1n leq_add2r size_poly_gt0. move: Hj; rewrite leq_eqVlt; case/predU1P => [<-{j} | Hj]; last first. rewrite !nth_default ?simp ?oppr0 ?(leq_trans Hr) //. by rewrite -{1}(subKn Hlt) leq_sub2r // (leq_trans Hr). move: Hr; rewrite leq_eqVlt ltnS; case/predU1P=> Hqq; last first. by rewrite !nth_default ?simp ?oppr0 // -{1}(subKn Hlt) leq_sub2r. rewrite /lead_coef Hqq polySpred // subSS subKn ?addrN //. by rewrite -subn1 leq_subLR add1n -Hqq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)