proposition: Lemma quarter_approx_le_abs_1 : forall (x : CR) (q : Q), Qabs (q - approximate x (Qpos2QposInf (1 # 4))) <= (3#4) -> Qabs q <= ` (CR_b (1 ↾ eq_refl) x + 1 ↾ eq_refl)%Qpos.
proof: Proof. intros. simpl. apply (Qle_trans _ _ _ (Qabs_triangle_reverse _ _)) in H. apply (Qplus_le_l _ _ (-Qabs (approximate x (Qpos2QposInf (1#4))))). apply (Qle_trans _ _ _ H). clear H q. pose proof (regFun_prf x (1#4)%Qpos (1#1)%Qpos). apply AbsSmall_Qabs in H. apply Qopp_le_compat in H. apply (Qplus_le_r _ _ (2#1)) in H. setoid_replace (2 + - (` ((1 # 4) ↾ eq_refl) + ` (1 ↾ eq_refl))) with (3#4) in H by reflexivity. rewrite <- Qplus_assoc, <- Qplus_assoc, Qplus_comm, Qplus_assoc. setoid_replace ((1#1)+(1#1)) with (2#1) by reflexivity. apply (Qle_trans _ _ _ H). clear H. rewrite <- Qplus_assoc. apply Qplus_le_r. setoid_replace (- Qabs (approximate x (Qpos2QposInf (1 # 4))) + Qabs (approximate x (Qpos2QposInf (1#1))))%Q with (- (Qabs (approximate x (Qpos2QposInf (1 # 4))) - Qabs (approximate x (Qpos2QposInf (1#1))))) by (unfold equiv, stdlib_rationals.Q_eq; ring). apply Qopp_le_compat, Qabs_triangle_reverse. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names