proposition: Lemma addXnE n p q : to_poly (addXn n p q) = to_poly p * 'X^n + to_poly q.
proof: Proof. elim: p n q => [a n q|a n' p ih n [b|b m q]] /=; simpC; first by rewrite addXn_constE. case: eqP => [->|/eqP n0]; first by rewrite expr0 mulr1 /= polyCD addrA. by rewrite /= /cast /cast_pos_nat /cast_nat_pos insubdK // -topredE /= lt0n. case: eqP => [->|/eqP no]. rewrite expr0 mulr1 /leq_op /leq_pos /eq_op /eq_pos. case: ifP => [/eqP ->|hneq] /=. by rewrite ih expr0 mulr1 mulrDl polyCD -!addrA [_ + (a%:P + _)]addrCA. rewrite -[(_ < _)%C]/((_ < _)%N). case hnm: (val n' < val m); rewrite /= ih polyCD mulrDl -!addrA ?expr0. rewrite mulr1 /= addr0 -mulrA -exprD [_ + (a%:P + _)]addrCA /cast. by rewrite /cast_pos_nat insubdK ?subnK -?topredE /= ?subn_gt0 // ltnW. rewrite -mulrA -exprD [_ + (a%:P + _)]addrCA /cast /cast_pos_nat. rewrite insubdK ?subnK // -?topredE /=; first by rewrite leqNgt hnm. rewrite subn_gt0 ltnNge leq_eqVlt hnm Bool.orb_false_r {hnm}. move/negbT: hneq; apply: contra; move/eqP=> heq; apply/eqP; exact: val_inj. rewrite !ih !addXn_constE expr0 mulr1 /= addr0 mulrDl -mulrA -exprD addnC. by rewrite -!addrA [b%:P + (_ + _)]addrCA [b%:P + _]addrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements pos hrel poly_op)