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