proposition: Lemma one_root2_translate {R : archiFieldType} (l : {poly R}) a b : one_root2 (translate_pol l a) b -> one_root2 l (a + b).
proof: Proof. move=> [x1 [k [x1a kp neg sl]]]; exists (a + x1), k; split => //. - by rewrite ltr_add2l. - move=> x abx xax1; rewrite (_ : x = x - a + a); last by rewrite addrNK. by rewrite -translate_polq; apply: neg; rewrite ?ltr_subr_addl ?ler_subl_addl. - move=> x y ax1x xy. have t z : z = (z - a) + a by rewrite addrNK. rewrite {2}(t y) {2}(t x). rewrite -!(translate_polq l) (_ : y - x = y - a - (x - a)); last first. by rewrite [x + _]addrC opprD opprK addrA addrNK. by apply: sl; rewrite ?ler_subr_addl ?ltr_le_sub. Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc