proposition: Lemma Qmid (x y: Q): x < y -> let mid := (1#2)%Qpos*(x+y) in x < mid /\ mid < y.
proof: Proof. Proof with auto; try reflexivity. intros. subst mid. split. setoid_replace x with (x * (1#2) + x * (1#2)) at 1 by (simpl; ring). setoid_replace ((1 # 2) * (x + y)) with (y * (1 # 2) + x * (1 # 2)) by (simpl; ring). apply Qplus_lt_l. apply Qmult_lt_compat_r... setoid_replace y with (y * (1#2) + y * (1#2)) at 2 by (simpl; ring). setoid_replace ((1 # 2) * (x + y)) with (x * (1 # 2) + y * (1 # 2)) by (simpl; ring). apply Qplus_lt_l. apply Qmult_lt_compat_r... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program