proposition: Lemma le_closed (e x: T): (forall d: Qpos, x <= e + from_Qpos d) -> x <= e.
proof: Proof. Proof with auto. unfold le. simpl. intros H q H0 r qr. destruct (Qpos_lt_plus qr) as [d E]. apply (H ((1#2)*d)%Qpos (q + (2#3)*from_Qpos d)%Qnn). apply (is_binop_bound Qplus) with q ((1#2)*from_Qpos d)%Qnn... simpl. apply Qplus_le_compat... apply Qmult_le_compat_r... discriminate. simpl. rewrite E. do 2 rewrite (Qplus_comm (`q)). apply Qplus_lt_l. simpl. rewrite <- (Qmult_1_l d). 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