proposition: Lemma split_interval (a1 a2 r1 r2 x : F) : 0 < r1 -> 0 < r2 -> `|a1 - a2| <= r1 + r2 -> (`|x - center (a1, r1) (a2, r2)| <= radius (a1, r1) (a2, r2)) = (`|x - a1| <= r1) || (`|x - a2| <= r2).
proof: Proof. move=> r1_gt0 r2_gt0 le_ar. rewrite /merge_intervals /=. set l : F := minr _ _; set u : F := maxr _ _. rewrite ler_pdivl_mulr ?gtr0E // -{2}[2%:R]ger0_norm ?ger0E //. rewrite -normrM mulrBl mulfVK ?pnatr_eq0 // ler_distl. rewrite opprB addrCA addrK (addrC (l + u)) addrA addrNK. rewrite -!mulr2n !mulr_natr !ler_muln2r !orFb. rewrite le_minl le_maxr !ler_distl /=. set le := <=%R; rewrite {}/le. have [] := lerP=> /= a1N; have [] := lerP=> //= a1P; have [] := lerP=> //= a2P; rewrite ?(andbF, andbT) //; symmetry. rewrite ltW // (le_lt_trans _ a1P) //. rewrite (monoLR (addrK _) (ler_add2r _)) -addrA. rewrite (monoRL (addNKr _) (ler_add2l _)) addrC. by rewrite (le_trans _ le_ar) // ler_normr opprB lexx orbT. rewrite ltW // (lt_le_trans a1N) //. rewrite (monoLR (addrK _) (ler_add2r _)) -addrA. rewrite (monoRL (addNKr _) (ler_add2l _)) addrC ?[r2 + _]addrC. by rewrite (le_trans _ le_ar) // ler_normr lexx. 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)