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