proposition: Lemma interval_middle_compat: forall lb ub x y, interval lb ub x -> interval lb ub y -> interval lb ub (middle x y).
proof: Proof. intros lb ub x y x_in_I y_in_I. split ; unfold middle, interval in *. replace lb with ((lb + lb) * /2) by field. unfold Rdiv ; apply Rmult_le_compat_r ; intuition (auto with real). replace ub with ((ub + ub) * /2) by field. unfold Rdiv ; apply Rmult_le_compat_r ; intuition (auto with real). Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics