proposition: Lemma changes1_alternate d (l : seq R) f : (size l <= d.+1)%N -> (forall i, (i < d.+1)%N -> (0 < f i)) -> changes (seqn0 l) = 1%N -> 0 <= (seqn0 l)`_0 = true -> alternate (\sum_(i < d.+1) (l`_i * f i *: 'X^(d - i))).
proof: Proof. elim: d l f => [| d IH] /=. case => /= [ | a [ | *]] // f cf _. case: (a != 0) => //=; by rewrite mulr0 ltxx addn0. case => [| a l] //= f; rewrite ltnS. case h: (a!=0) => //=; last first. rewrite -[X in 0 <= X]/((seqn0 l)`_0) => h1 h2 h3 h4. rewrite big_ord_recl /=. have := negbFE h => /eqP => ->; rewrite mul0r scale0r add0r. have t : forall i : 'I_d.+1, true -> l`_i * f (bump 0 i) *: 'X^(d.+1 - bump 0 i) = l`_i * f (i.+1) *: 'X^(d - i). by move=> i /=; rewrite /bump leq0n add1n subSS. rewrite (eq_bigr _ t) {t}. have h2' : forall i : nat, (i < d.+1)%N -> (0 < f i.+1). by move=> i ci; apply: h2; rewrite ltnS. by apply: IH h2' _ _. case alt: (a * head 0 (seqn0 l) < 0)%R; last first. rewrite add0n => h1 h2 h3 h4. have h2' : forall i : nat, (i < d.+1)%N -> (0 < f i.+1). by move=> i ci; apply: h2; rewrite ltnS. have alt' : alternate (\sum_(i < d.+1) (l`_i * f i.+1) *: 'X^(d - i)). apply: (IH l (fun i => f i.+1)) => //. have agt0 : 0 < a by rewrite lt_neqAle eq_sym (negbTE h). rewrite -(ler_pmul2l agt0) mulr0 leNgt; apply: negbT; exact alt. rewrite big_ord_recl subn0 nth0 /= addrC; apply: alternate_r => //. rewrite pmulr_lgt0; first by rewrite lt_neqAle eq_sym h h4. by apply: h2. have asl : forall i : 'I_d.+1, (size (('X^(d.+1 - bump 0 i):{poly R})) <= d.+1)%N. by move=> i; rewrite /bump leq0n add1n subSS size_polyXn ltnS leq_subr. apply: size_weighted_sum_leq=> i _; apply: asl. rewrite add1n; move=> sl cf [c0] ap. have negl : head 0 (seqn0 l) < 0. have ap' : 0 < a by rewrite lt_neqAle eq_sym h ap. by rewrite -(ltr_pmul2l ap') mulr0 alt. have int: head 0 (seqn0 l) != 0 by rewrite neq_lt negl. move/seqn0_last: (int) => [l1 [x [l2 /andP [/eqP p1 /andP[p2 p3]]]]]. apply/alternate_P; rewrite /= -/R. have cfp : forall j, (j < d.+2)%N -> (\sum_(i < d.+2) ((a :: l)`_i * f i) *: 'X^(d.+1 - i))`_j = ((a :: l)`_(d.+1 - j) * f (d.+1 - j)%N). move=> j cj. have cut1 : (0 <= d.+1 - j)%N by rewrite leq0n. have cut2 : (d.+1 - j <= d.+2)%N. by rewrite (leq_trans _ (ltnW (ltnSn d.+1))) // leq_subr. rewrite -(big_mkord (fun i => true) (fun i => ((a :: l)`_i * f i) *: 'X^(d.+1 - i))). rewrite (big_cat_nat _ xpredT _ cut1 cut2) /= coef_add_poly. have cut3 : (d.+1 - j <= (d.+1 - j).+1)%N by rewrite leqnSn. have cut4 : ((d.+1 - j) < d.+2)%N by rewrite ltnS leq_subr. rewrite (big_cat_nat _ xpredT _ cut3 cut4) /= coef_add_poly. rewrite big_nat1 coefZ subKn; last by rewrite -ltnS. rewrite coefXn eqxx mulr1 [X in X + (_ + _)](_ : _ = 0). rewrite add0r [X in _ + X](_ : _ = 0); first by rewrite addr0. rewrite nth_default //. apply: size_weighted_sum_leq=> i; rewrite mem_index_iota => /andP [ci c']. rewrite size_polyXn. move: ci; rewrite -(ltn_add2r j) subnK; last by rewrite -ltnS. move=> ci; rewrite -(ltn_add2r i) subnK; first by rewrite addnC. by rewrite -ltnS. have t : forall i, (0 <= i < d.+1 - j)%N -> ((a :: l)`_i * f i) *: 'X^(d.+1 - i) = ((a :: l)`_i * f i) *: 'X^(d - j - i) * 'X^j.+1. move=> i /andP [_ ci]; rewrite -scalerAl -exprD addnS subnAC subnK. by rewrite subSn // -ltnS (leq_trans ci). rewrite -(leq_add2r i) subnK; last first. by rewrite -ltnS (leq_trans ci). move: ci; rewrite -(ltn_add2r j) subnK. by rewrite ltnS addnC. by rewrite -ltnS. by rewrite (@eq_big_nat _ _ _ _ _ _ _ t) -big_distrl coefMXn leqnn. exists (mkseq (fun i => 0) (d.+1 - size l)++(rev l2)), (x * f (size l1).+1), (mkseq (fun i => (rev l1)`_i * f ((size l1) - i)%N) (size l1)), (a * f 0%N), [::]. have am : all_eq0 (mkseq (fun _ => (0:R)) (d.+1 - size l)). rewrite /all_eq0; apply/(all_nthP 0); rewrite size_mkseq=> i ci. by rewrite nth_mkseq. have apos : 0 < a * f 0%N. by apply: mulr_gt0; first rewrite lt_neqAle ap eq_sym h //; apply: cf. rewrite /all_eq0 /all_le0 all_cat -!all_rev -/(all_eq0 l2) p3 /=. have al : all_le0 l by apply: first_neg_no_change_all_le0. rewrite [all _ (mkseq _ _)]am apos /=. have sl' : (size l1 + size l2 <= d)%N. by move: sl; rewrite p1 size_cat /= addnS ltnS. have sl1d : (size l1 <= d)%N. by apply: leq_trans sl'; apply leq_addr. have -> : x * f (size l1).+1 < 0. rewrite pmulr_llt0; last by apply: cf; rewrite !ltnS. rewrite lt_neqAle; rewrite p2 /=. by move/allP: al=> al; apply al; rewrite p1 mem_cat in_cons eqxx orbT. split => //; last split=>//. have st : size (a * f 0%N *: 'X^d.+1) = d.+2. rewrite -mul_polyC size_Cmul ?size_polyXn // mulf_neq0 //. by rewrite neq_lt cf ?orbT. set sg := \sum_(_ < _) _; have st' : size sg = d.+2. rewrite /sg big_ord_recl /= subn0 size_addl; first by []. rewrite st ltnS size_weighted_sum_leq ?st //. by move=> [i C] _; rewrite /bump add1n subSS size_polyXn ltnS leq_subr. apply: (@eq_from_nth _ 0). move:sl; rewrite p1 !size_cat /= !size_cat /= !size_rev !addnS addn0=> T. by rewrite !size_mkseq subSS -addnA [(size l2 + _)%N]addnC subnK. move=> i; rewrite st' => ci; rewrite cfp // {st' sg st al apos am cfp}. rewrite nth_cat size_cat size_mkseq size_rev. case b1 : (i < d.+1 - size l + size l2)%N. rewrite nth_cat size_mkseq. case b2 : (i < d.+1 - size l)%N. rewrite nth_mkseq // nth_default ?mul0r //=. move: b2; rewrite -(ltn_add2r (size l)) subnK // => b2. by rewrite -(ltn_add2r i) subnK // addnC. have b2' : (d.+1 - size l <= i)%N by rewrite leqNgt b2. rewrite nth_rev; last first. by rewrite -(ltn_add2r (d.+1 - size l)) subnK // addnC. case l2c : (l2) => [ | b l3] /=; first by move: b1; rewrite l2c addn0 b2. move: p3 {b2}; rewrite /all_eq0=>/all_nthP=> l20. rewrite -l2c (eqP (l20 0 _ _)); last first. by rewrite subSS l2c /= ltnS leq_subr. have b1' : (i < d - size l1)%N. move: b1; rewrite p1 size_cat /= addnS subSS subnDA subnK //. by rewrite -(leq_add2r (size l1)) subnK // addnC. have di1 : (i <= d)%N by rewrite (leq_trans (ltnW b1')) // leq_subr. rewrite subSn //= p1 nth_cat. have dil1 : (d - i < size l1)%N = false. apply: negbTE; rewrite -leqNgt -(leq_add2r i) subnK//. move: b1; rewrite -(ltn_add2l (size l1)) => b1. rewrite -ltnS (leq_trans b1) // p1 size_cat /= addnS subSS. by rewrite !(addnC (size l1)) -addnA subnK // addnC. rewrite dil1; move/negbT: dil1; rewrite -leqNgt=>dil1. rewrite -subnDA addnC subnDA -subnSK //= (eqP (l20 _ _ _)) ?mul0r //. rewrite -(ltn_add2r i.+1) subnK // addnS ltnS -leq_subLR. by rewrite (leq_trans _ b2') // p1 size_cat /= addnS subSS subnDA. move=>{p3 p2}. move/negbT: b1; rewrite -leqNgt leq_eqVlt => /predU1P[b1 {ci}|b1]. rewrite b1 subnn p1 /= -b1 p1 size_cat /= addnS subSS [(d - _)%N]subnDA. rewrite subnK; last first. by rewrite -(leq_add2r (size l1)) subnK // addnC. by rewrite subSn ?leq_subr // subKn //= nth_cat ltnn subnn /=. have sl2dml1: (size l2 <= d - size l1)%N. by rewrite -(leq_add2r (size l1)) subnK // addnC. have dml1i : (d - size l1 < i)%N. by apply: leq_trans b1; rewrite p1 size_cat /= addnS subSS subnDA subnK. rewrite -[(i - _)%N]subnSK //= nth_cat size_mkseq -subnDA. rewrite subnSK //. case b2 : (i - (d.+1 - size l + size l2) <= size l1)%N. rewrite nth_mkseq; last by rewrite subnSK. move: (b2); rewrite -(leq_add2r (d.+1 - size l + size l2)). rewrite subnK; last by rewrite ltnW. rewrite addnC p1 size_cat /= addnS subSS subnDA subnK // subnK // => b2'. rewrite nth_rev; last first. by rewrite -(ltn_add2r (d - size l1).+1) subnK // addnS addnC subnK. rewrite subnSK // subSn //= subnBA; last by rewrite ltnW. rewrite addnC subnK // subnBA // addnS addnC subnK // nth_cat. have dmil1 : (d - i < size l1)%N. rewrite -(ltn_add2r i) subnK //; move: dml1i. by rewrite -(ltn_add2r (size l1)) subnK // addnC. by rewrite dmil1 subSn. move/negbT: b2; rewrite -ltnNge=> b2. have difinal : i = d.+1. apply: anti_leq; apply/andP; split; first by rewrite -ltnS. move: b2; rewrite -(ltn_add2r (d.+1 - size l + size l2)). rewrite subnK; last by rewrite ltnW. by rewrite p1 size_cat /= addnS subSS subnDA subnK // addnC subnK. rewrite difinal subnn addSn subSS p1 size_cat /= addnS subnDA subSS. rewrite [(d - (size l1 + size l2))%N]subnDA subnK // subnBA //. by rewrite addKn subnn. apply/(all_nthP 0); rewrite size_mkseq => i C; rewrite nth_mkseq // pmulr_lle0. move: al; rewrite /all_le0 p1 all_cat => /andP [al1 _]; rewrite nth_rev //. by move/(all_nthP 0): al1 => -> //; rewrite subnSK // leq_subr. apply: cf; rewrite ltnS (leq_trans _ (ltnW (ltnSn _))) ?(leq_trans _ sl1d) //. by rewrite leq_subr. 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