proposition: Lemma one_root2_shift p a b: one_root2 (p \shift a) b -> one_root2 p (a + b).
proof: Proof. move=> [ck [/andP [x1a kp] neg sl]]. exists (a + ck.1,ck.2); split. by rewrite ltr_add2l x1a kp. move=> x /= abxax1; rewrite -(addrNK a x) - horner_shift_poly. by rewrite neg // ltr_subr_addl ler_subl_addl. move=> x y /= axy. have aux: y - x = y - a - (x - a). by rewrite opprD addrAC -!addrA opprK addrN addr0. rewrite -{2} (addrNK a x) -{2} (addrNK a y) -!(horner_shift_poly a _) aux. by apply: sl; rewrite ? ler_add2r // ler_subr_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