proposition: Lemma aq_lt_mid (x y : Q) : (x < y)%Q → { z : AQ | (x < 'z ∧ 'z < y)%Q }.
proof: Proof. Proof with auto with qarith. intros E. destruct (Qpos_sub _ _ E) as [γ Eγ]. exists (app_inverse (cast AQ Q) ((1#2) * (x + y)) ((1#3) * γ)%Qpos)%Q. split. apply Qlt_le_trans with (x + (1#6) * proj1_sig γ)%Q. rewrite <-(rings.plus_0_r x) at 1. apply Qplus_lt_r... assert (Qeq (x + (1 # 6) * ` γ) ((1 # 2) * (x + y) - proj1_sig ((1 # 3) * γ)%Qpos)%Q). { rewrite Eγ. simpl. ring. } rewrite H5. clear H5. simpl. apply (in_Qball (proj1_sig ((1#3)*γ)%Qpos)), ball_sym, dense_inverse. apply Qle_lt_trans with (y - (1#6) * proj1_sig γ)%Q. assert (Qeq (y - (1 # 6) * ` γ) ((1 # 2) * (x + y) + proj1_sig ((1 # 3) * γ)%Qpos)). { rewrite Eγ. simpl. ring. } rewrite H5. clear H5. simpl. apply (in_Qball (proj1_sig ((1#3)*γ)%Qpos)), ball_sym, dense_inverse. apply (Qlt_le_trans _ (y-0)). apply Qplus_lt_r. apply Qopp_Qlt_0_r... unfold Qminus. rewrite Qplus_0_r. apply Qle_refl. Defined.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program CoRN.model.totalorder.QposMinMax MathClasses.misc.workaround_tactics CoRN.stdlib_omissions.Q CoRN.util.Qdlog CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.classes.Qclasses CoRN.model.totalorder.QMinMax CoRN.algebra.RSetoid CoRN.metric2.MetricMorphisms MathClasses.orders.minmax MathClasses.orders.dec_fields MathClasses.theory.abs MathClasses.theory.shiftl MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders