proposition: Lemma one_root1_shift p a b c: one_root1 (shift_poly c p) a b -> one_root1 p (c + a) (c + b).
proof: Proof. move=> [x1 [x2 [k [/and4P [ax1 x1x2 x2b kp] pos neg sl]]]]. exists (c + x1); exists (c + x2); exists k. rewrite ! ltr_add2l; split => //; first by apply /and4P. move=> x cp; rewrite - (addrNK c x). rewrite -horner_shift_poly pos ? ler_sub_addl ? ltr_sub_addl //. move=> x cp; rewrite - (addrNK c x). by rewrite -horner_shift_poly neg // ltr_subr_addl ltr_subl_addl. move=> x y cx1x xy ycx2. have aux: y - x = y - c - (x - c). by rewrite [x + _]addrC opprD opprK addrA addrNK. rewrite -{2} (addrNK c x) -{2} (addrNK c y) aux -!(horner_shift_poly c _). by rewrite sl ? ler_add2r // ?ler_subr_addr? ler_subl_addr // addrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol