proposition: Lemma middle_is_in_the_middle': forall x y, x <= y -> x <= middle x y <= y.
proof: Proof. intros x y xley ; destruct (Req_dec x y). subst ; rewrite middle_identity ; auto. split ; left ; apply middle_is_in_the_middle, Rle_neq_lt ; assumption. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics