proposition: Lemma interval_open_restriction : forall lb ub a b, open_interval lb ub a -> open_interval lb ub b -> included (interval a b) (open_interval lb ub).
proof: Proof. intros lb ub a b a_in b_in x x_in ; split. eapply Rlt_le_trans ; [eapply a_in | eapply x_in]. eapply Rle_lt_trans ; [eapply x_in | eapply b_in]. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics