proposition: Lemma ch0_correct l d a b q : a < b -> q != 0 -> q = \sum_(i < d.+1) l`_i *: bernp a b d i -> changes (seqn0 l) = 0%N -> no_root_for (horner q) a b.
proof: Proof. move=> ab. wlog : l q / 0 <= head 0 (seqn0 l). move=> wlh qn0 qq ch. case pos : (0 <= head 0 (seqn0 l)); first by apply: (wlh l) => //. have ssn0 : (0 < size (seqn0 l))%N. rewrite lt0n; apply/negP=> s0. case/negP: qn0; rewrite qq big1 //. move=> i _; case sli: (size l <= i)%N. by rewrite nth_default ?scale0r. have : all_eq0 l by rewrite -all_eq0_seqn0 -nth0 nth_default // (eqP s0). move/negbT: sli; rewrite -ltnNge=> sli /allP l0. by have := mem_nth 0 sli => /l0/eqP=> li0; rewrite li0 scale0r. move: ch; rewrite -changes_oppr -seqn0_oppr => ch. move/negbT: pos; rewrite -ltNge -oppr_gt0 -nth0 -(nth_map 0 0) // nth0. rewrite -seqn0_oppr=>pos. have ssn0' : (0 < size (seqn0 [seq -x | x <- l]))%N. by rewrite seqn0_oppr size_map. move: qn0; rewrite -oppr_eq0 => qn0. have := refl_equal (-q); rewrite [X in _ = - X]qq -[X in _ = -X]mul1r {qq}. rewrite -mulNr big_distrr /=. have t : forall i : 'I_d.+1, true -> -1 * (l`_i *: bernp a b d i) = [seq -x | x <- l]`_i *: bernp a b d i. move=> i _; case ci : (i < size l)%N. rewrite (nth_map 0) // -[-1]/(-(1%:P)) -polyCN mul_polyC scalerA. by rewrite mulNr mul1r. move/negbT: ci; rewrite -leqNgt=> ci. rewrite !nth_default //; first by rewrite !scale0r mulr0. by rewrite size_map. rewrite (eq_bigr _ t) => qq {t ssn0}. have {wlh qq ch qn0 pos ssn0'} := wlh _ _ (ltW pos) qn0 qq ch. by move=> nx x inx; rewrite -[q.[x]]opprK -hornerN oppr_eq0 nx. move=> h qn0 qq ch x inx; apply /negP; rewrite qq. rewrite horner_sum psumr_eq0 /=. move=> al0; case/negP: qn0; rewrite qq. rewrite big1 //; move => i _; rewrite [l`_i](_ : _ = 0) ?scale0r //. have : l`_i * (bernp a b d i).[x] == 0. by have := (allP al0 i (mem_index_enum _)); rewrite hornerZ. rewrite mulf_eq0. case: i => i /=; rewrite ltnS => ci. have := bernp_gt0 ci inx; set bf := (_.[_]) => b0. have bn0 : (bf != 0) by rewrite neq_lt b0 orbT. by rewrite (negbTE bn0) orbF => /eqP. move=> i _; rewrite hornerZ. apply: mulr_ge0; last first. by apply/ltW/bernp_gt0=> //; case i. case sli: (i < size l)%N; last first. by move/negbT: sli; rewrite -leqNgt=> sli; rewrite nth_default //. by move/allP: (first_pos_no_change_all_ge0 h ch)=> t; apply/t/mem_nth. 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