proposition: Lemma middle_lt_lt_neg_lt : forall x y, x < 0 -> y < 0 -> middle x y < 0.
proof: Proof. intros x y x_neg y_neg ; unfold middle, Rdiv ; replace 0 with ((x + y) * 0) by ring ; apply Rmult_lt_gt_compat_neg_l ; lra. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics