proposition: Lemma Qmult_wiggle (x y z : Q): 0 <= x -> 0 <= y -> x * y < z -> exists e : Qpos, (x + e) * y < z.
proof: Proof. Proof with auto with *. intros xnn ynn xyz. destruct (Qdec_sign y) as [[A|B]|C]. exfalso. apply Qle_not_lt with 0 y... destruct (Qpos_lt_plus xyz) as [e E]. exists (e / ((2#1) * exist (Qlt 0) y B))%Qpos. rewrite E. rewrite Qmult_plus_distr_l. do 2 rewrite (Qplus_comm (x * y)). apply Qplus_lt_l. simpl. setoid_replace (e * / ((2 # 1) * y) * y) with (/ (2 # 1) * e) by (simpl; field)... rewrite <- (Qmult_1_l e) at 2. apply Qmult_lt_compat_r... exists (1#1)%Qpos. revert xyz. rewrite C, Qmult_0_r, Qmult_0_r... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program