proposition: Lemma middle_lt_le_pos_lt : forall x y, 0 < x -> 0 <= y -> 0 < middle x y.
proof: Proof. intros x y x_pos y_pos ; rewrite middle_comm ; apply middle_le_lt_pos_lt ; assumption. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics