proposition: Lemma one_root1_scale p a b c: 0 < c -> one_root1 (p \scale c) a b -> one_root1 p (c * a) (c * b).
proof: Proof. move=> cp [x1 [x2 [k [/and4P [ax1 x1x2 x2b kp] pos neg sl]]]]. exists (c * x1); exists (c * x2); exists (k / c). have tc : 0 < c^-1 by rewrite invr_gt0. rewrite !(ltr_pmul2l cp). have t: forall z, z = c * (z / c). by move=> z; rewrite [c * _]mulrC mulfVK //;move: cp;rewrite lt0r => /andP []. split => //; first by apply/and4P; split => //; apply:mulr_gt0. move=> x cpp; rewrite (t x) - horner_scaleX_poly; apply: pos. by rewrite ltr_pdivl_mulr // mulrC ler_pdivr_mulr //(mulrC x1). move=> x cpp. rewrite (t x) -horner_scaleX_poly neg //. by rewrite ltr_pdivl_mulr // mulrC ltr_pdivr_mulr // (mulrC b). move=> x y cx1x xy ycx2; rewrite -mulrA mulrDr mulrN ![c^-1 * _]mulrC {2}(t x) {2}(t y) -!(horner_scaleX_poly _ p); apply: sl. by rewrite ler_pdivl_mulr // mulrC. by rewrite ler_wpmul2r // ltW. by rewrite ler_pdivr_mulr // mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol