proposition: Lemma addXn_constE n a q : to_poly (addXn_const n a q) = a%:P * 'X^n + to_poly q.
proof: Proof. elim: q n => [b [|n]|b m q' ih n] /=; simpC; first by rewrite polyCD expr0 mulr1. by rewrite /cast /cast_pos_nat insubdK. case: eqP => [->|/eqP n0] /=; first by rewrite polyCD expr0 mulr1 addrCA. case: eqP => [hn|hnc] /=; first by rewrite ih expr0 mulr1 -hn mulrDl -addrA. rewrite [(_ < _)%C]/((_ < _)%N) subn_eq0. case hnm: (n < cast m). rewrite /= /cast /cast_nat_pos /cast_pos_nat. rewrite insubdK -?topredE /= ?lt0n // mulrDl -mulrA -exprD addrCA -addrA. by rewrite ?insubdK -?topredE /= ?subn_gt0 ?lt0n ?subnK // ltnW. by rewrite /= ih mulrDl -mulrA -exprD subnK ?addrA // leqNgt hnm. 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)