proposition: Lemma interval_open_interval : forall x y z, interval x y z -> x <> z -> y <> z -> open_interval x y z.
proof: Proof. intros x y z [xz zy] x_neq y_neq ; split ; apply Rle_neq_lt ; auto. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity