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