proposition: Lemma included_open_interval_interval : forall a b, included (open_interval a b) (interval a b).
proof: Proof. intros a b x [x_l x_r] ; split ; left ; assumption. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics