proposition: Lemma Qplus_wiggle (x y z : Q): 0 <= x -> 0 <= y -> x + y < z -> exists e: Qpos, x + e + y < z.
proof: Proof. Proof with auto. intros ?? E. destruct (Qpos_lt_plus E) as [e F]. exists ((1#2) * e)%Qpos. rewrite F. simpl. ring_simplify. apply Qplus_lt_l. do 2 rewrite (Qplus_comm x). apply Qplus_lt_l. rewrite <- (Qmult_1_l e) at 2. apply Qmult_lt_compat_r... reflexivity. Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program