proposition: Lemma merge_mono p a1 a2 r1 r2 : 0 < r1 -> 0 < r2 -> `|a1 - a2| <= (r1 + r2) -> strong_mono p a1 r1 -> strong_mono p a2 r2 -> strong_mono p (center (a1, r1) (a2, r2)) (radius (a1, r1) (a2, r2)).
proof: Proof. move=> r1_gt0 r2_gt0 har sm1; wlog : p sm1 / accr_pos p a1 r1. move=> hwlog; case: (sm1); first exact: hwlog. move=> accr_p smp; rewrite -[p]opprK; apply: strong_monoN. apply: hwlog=> //; do ?exact: strong_monoN. exact: accr_posN. case=> [[k1 k1_gt0 hk1]] h1. move=> [] accr2_p; last first. set m := (r2 * a1 + r1 * a2) / (r1 + r2). have pm_gt0 := h1 m. case: accr2_p=> [_] /(_ m) pm_lt0. suff: 0 < 0 :> F by rewrite ltxx. have r_gt0 : 0 < r1 + r2 by rewrite ?addr_gt0. apply: (lt_trans (pm_gt0 _) (pm_lt0 _)). rewrite -(@ler_pmul2l _ (r1 + r2)) //. rewrite -{1}[r1 + r2]ger0_norm ?(ltW r_gt0) //. rewrite -normrM mulrBr /m mulrC mulrVK ?unitfE ?gt_eqF //. rewrite mulrDl opprD addrA addrC addrA addKr. rewrite distrC -mulrBr normrM ger0_norm ?(ltW r1_gt0) //. by rewrite mulrC ler_wpmul2r // ltW. rewrite -(@ler_pmul2l _ (r1 + r2)) //. rewrite -{1}[r1 + r2]ger0_norm ?(ltW r_gt0) //. rewrite -normrM mulrBr /m mulrC mulrVK ?unitfE ?gt_eqF //. rewrite mulrDl opprD addrA addrK. rewrite -mulrBr normrM ger0_norm ?(ltW r2_gt0) //. by rewrite mulrC ler_wpmul2r // ltW. case: accr2_p=> [[k2 k2_gt0 hk2]] h2. left; split; last by move=> x; rewrite split_interval // => /orP [/h1|/h2]. exists (minr k1 k2); first by rewrite lt_minr k1_gt0. move=> x y neq_xy; rewrite !split_interval //. wlog lt_xy: x y neq_xy / y < x. move=> hwlog; have [] := ltrP y x; first exact: hwlog. rewrite le_eqVlt (negPf neq_xy) /= => /hwlog hwlog' hx hy. rewrite -mulrNN -!invrN !opprB. by apply: hwlog'; rewrite // eq_sym. move=> {h1} {h2} {sm1}. wlog le_xr1 : a1 a2 r1 r2 k1 k2 r1_gt0 r2_gt0 k1_gt0 k2_gt0 har hk1 hk2 / `|x - a1| <= r1. move=> hwlog h; move: (h)=> /orP [/hwlog|]; first exact. move=> /(hwlog a2 a1 r2 r1 k2 k1) hwlog' ley; rewrite minC. by apply: hwlog'; rewrite 1?orbC // distrC [r2 + _]addrC. move=> _. have [le_yr1|gt_yr1] := (lerP _ r1)=> /= [_|le_yr2]. by rewrite lt_minl hk1. rewrite ltr_pdivl_mulr ?subr_gt0 //. pose z := a1 - r1. have hz1 : `|z - a1| <= r1 by rewrite addrC addKr normrN gtr0_norm. have gt_yr1' : y + r1 < a1. rewrite addrC; move: gt_yr1. rewrite (monoLR (addrNK _) (ltr_add2r _)). rewrite /z ltr_normr opprB=> /orP[|-> //]. rewrite (monoRL (addrK a1) (ltr_add2r _))=> /lt_trans /(_ lt_xy). by rewrite ltNge addrC; move: le_xr1; rewrite ler_distl=> /andP [_ ->]. have lt_yz : y < z by rewrite (monoRL (addrK _) (ltr_add2r _)). have hz2 : `|z - a2| <= r2. move: (har); rewrite ler_norml=> /andP [la ua]. rewrite addrAC ler_distl ua andbT. rewrite -[a1](addrNK y) -[_ - _ + _ - _]addrA. rewrite ler_add //. by rewrite (monoRL (addrK _) (ler_add2r _)) addrC ltW. by move: le_yr2; rewrite ler_norml=> /andP[]. have [<-|neq_zx] := eqVneq z x. by rewrite -ltr_pdivl_mulr ?subr_gt0 // lt_minl hk2 ?orbT // gt_eqF. have lt_zx : z < x. rewrite lt_neqAle neq_zx /=. move: le_xr1; rewrite distrC ler_norml=> /andP[_]. by rewrite !(monoLR (addrK _) (ler_add2r _)) addrC. rewrite -{1}[x](addrNK z) -{1}[p.[x]](addrNK p.[z]). rewrite !addrA -![_ - _ + _ - _]addrA mulrDr ltr_add //. rewrite -ltr_pdivl_mulr ?subr_gt0 //. by rewrite lt_minl hk1 ?gt_eqF. rewrite -ltr_pdivl_mulr ?subr_gt0 //. by rewrite lt_minl hk2 ?orbT ?gt_eqF. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)