proposition: Lemma one_root1_translate {R : archiFieldType} (l : {poly R}) a b c : one_root1 (translate_pol l c) a b -> one_root1 l (c + a) (c + b).
proof: Proof. move=> [x1 [x2 [k [[ax1 x1x2 x2b kp] pos neg sl]]]]. exists (c + x1), (c + x2), k; split. - by rewrite !ltr_add2l. - move=> x cax xcx1; rewrite (_ : x = x - c + c); last by rewrite addrNK. by rewrite -translate_polq; apply pos; rewrite ?ltr_subr_addl ?ler_subl_addl. - move=> x cx2x xcb; rewrite (_ : x = x - c + c); last by rewrite addrNK. rewrite -translate_polq; apply: neg; rewrite -?ler_addlA //. by rewrite ltr_subr_addl. by rewrite ltr_subl_addl. - move=> x y cx1x xy ycx2. have t z : z = (z - c) + c by rewrite addrNK. rewrite {2}(t x) {2}(t y) (_ : y - x = y - c - (x - c)); last first. by rewrite [x + _]addrC opprD opprK addrA addrNK. rewrite -!(translate_polq l); apply: sl; rewrite ?ler_add2l. + by rewrite ltr_subr_addl. + by rewrite ler_sub. + by rewrite ltr_subl_addl. Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc