proposition: Lemma alternate_r d (p : {poly R}) a : ( 0 < a) -> alternate p -> (size p <= d)%N -> alternate (p + a *: 'X ^+ d).
proof: Proof. move=> a0 /alternate_P [l1 [x [l2 [y [l3 [P1 P2 P3 P4]]]]]] ps. apply/alternate_P; exists l1, x, l2, y. exists (l3 ++ (mkseq (fun i => 0) (d - size p)) ++ [:: a]). split => //; first last. case: P4 => P4 P5 P6; split=> //. rewrite !all_ge0_cat P6 andTb; apply/andP; split; last by rewrite /= ltW. by apply/(all_nthP 0); move => i; rewrite size_mkseq => W; rewrite nth_mkseq. set m := mkseq _ _; set l := _ ++ _. have reorg : l = p ++ m ++ [:: a] by rewrite P1 /m -!(catA, cat_cons). have saxd : size (a *: 'X^d) = d.+1. by rewrite -mul_polyC size_Cmul ?size_polyXn; last rewrite neq_lt a0 orbT. have spax : size (p + a *: 'X^d) = d.+1. by rewrite addrC size_addl // saxd ltnS. have sreo : size (p ++ m) = d by rewrite size_cat /m size_mkseq addnC subnK. apply: (@eq_from_nth _ 0). by rewrite spax reorg catA size_cat sreo /= addn1. move=> i; rewrite spax ltnS leq_eqVlt=> ib; rewrite coef_add_poly coefZ. case/predU1P: ib => [->|iltd]. rewrite [p`_d]nth_default // add0r coefXn eqxx mulr1 reorg catA. by rewrite nth_cat sreo ltnn subnn. move: (iltd); rewrite coefXn ltn_neqAle=> /andP [df _]; rewrite (negbTE df). rewrite mulr0 addr0 reorg catA nth_cat sreo iltd nth_cat. case tst: (i < size p)%N => //. rewrite /m nth_mkseq. by rewrite nth_default // leqNgt tst. by rewrite ltn_subRL addnC subnK // leqNgt tst. 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