proposition: Lemma Ball_in_inter : forall c1 c2 r1 r2 x, Boule c1 r1 x -> Boule c2 r2 x -> {r3 : posreal | forall y, Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y}.
proof: Proof. intros c1 c2 [r1 r1p] [r2 r2p] x; unfold Boule; simpl; intros in1 in2. assert (Rmax (c1 - r1)(c2 - r2) < x). { apply Rmax_lub_lt;[revert in1 | revert in2]; intros h; apply Rabs_def2 in h; destruct h as [_ u]; apply (fun h => Rplus_lt_reg_r _ _ _ (Rle_lt_trans _ _ _ h u)), Req_le; ring. } assert (x < Rmin (c1 + r1) (c2 + r2)). { apply Rmin_glb_lt;[revert in1 | revert in2]; intros h; apply Rabs_def2 in h; destruct h as [u _]; apply (fun h => Rplus_lt_reg_r _ _ _ (Rlt_le_trans _ _ _ u h)), Req_le; ring. } assert (t: 0 < Rmin (x - Rmax (c1 - r1) (c2 - r2)) (Rmin (c1 + r1) (c2 + r2) - x)). { apply Rmin_glb_lt; apply Rlt_0_minus; assumption. } exists (mkposreal _ t). apply Rabs_def2 in in1; destruct in1. apply Rabs_def2 in in2; destruct in2. assert (c1 - r1 <= Rmax (c1 - r1) (c2 - r2)) by apply Rmax_l. assert (c2 - r2 <= Rmax (c1 - r1) (c2 - r2)) by apply Rmax_r. assert (Rmin (c1 + r1) (c2 + r2) <= c1 + r1) by apply Rmin_l. assert (Rmin (c1 + r1) (c2 + r2) <= c2 + r2) by apply Rmin_r. assert (Rmin (x - Rmax (c1 - r1) (c2 - r2)) (Rmin (c1 + r1) (c2 + r2) - x) <= x - Rmax (c1 - r1) (c2 - r2)) by apply Rmin_l. assert (Rmin (x - Rmax (c1 - r1) (c2 - r2)) (Rmin (c1 + r1) (c2 + r2) - x) <= Rmin (c1 + r1) (c2 + r2) - x) by apply Rmin_r. simpl. intros y h; apply Rabs_def2 in h; destruct h as [h h']. apply Rmin_Rgt in h; destruct h as [cmp1 cmp2]. apply Rplus_lt_reg_r in cmp2; apply Rmin_Rgt in cmp2. rewrite Ropp_Rmin, Ropp_minus_distr in h'. apply Rmax_Rlt in h'; destruct h' as [cmp3 cmp4]; apply Rplus_lt_reg_r in cmp3; apply Rmax_Rlt in cmp3; split; apply Rabs_def1. - apply (fun h => Rplus_lt_reg_l _ _ _ (Rle_lt_trans _ _ _ h (proj1 cmp2))), Req_le; ring. - apply (fun h => Rplus_lt_reg_l _ _ _ (Rlt_le_trans _ _ _ (proj1 cmp3) h)), Req_le; ring. - apply (fun h => Rplus_lt_reg_l _ _ _ (Rle_lt_trans _ _ _ h (proj2 cmp2))), Req_le; ring. - apply (fun h => Rplus_lt_reg_l _ _ _ (Rlt_le_trans _ _ _ (proj2 cmp3) h)), Req_le; ring. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra