proposition: Lemma Boule_convex : forall c d x y z, Boule c d x -> Boule c d y -> x <= z <= y -> Boule c d z.
proof: Proof. intros c d x y z bx b_y intz. unfold Boule in bx, b_y; apply Rabs_def2 in bx; apply Rabs_def2 in b_y; apply Rabs_def1; [apply Rle_lt_trans with (y - c);[apply Rplus_le_compat_r|]| apply Rlt_le_trans with (x - c);[|apply Rplus_le_compat_r]];tauto. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra