proposition: Lemma CRabs_AbsSmall : forall a b : CR, (CRabs b <= a)%CR <-> (-a <= b /\ b <= a)%CR.
proof: Proof. split. - intros. split. + intro e. simpl. unfold Cap_raw. simpl. specialize (H e). simpl in H. unfold Cap_raw in H. simpl in H. apply (Qle_trans _ _ _ H). rewrite Qopp_involutive, Qplus_comm. apply Qplus_le_l. rewrite <- (Qopp_involutive (approximate b ((1#2)*e)%Qpos)) at 2. apply Qopp_le_compat. rewrite <- Qabs_opp. apply Qle_Qabs. + intro e. simpl. unfold Cap_raw. simpl. specialize (H e). simpl in H. unfold Cap_raw in H. simpl in H. apply (Qle_trans _ _ _ H). apply Qplus_le_r, Qopp_le_compat, Qle_Qabs. - intros [H H0]. intro e. simpl. unfold Cap_raw. simpl. specialize (H e). simpl in H. unfold Cap_raw in H. simpl in H. specialize (H0 e). simpl in H0. unfold Cap_raw in H0. simpl in H0. apply (Qplus_le_l _ _ (Qabs (approximate b ((1 # 2) * e)%Qpos) + proj1_sig e)). simpl. ring_simplify. apply Qabs_Qle_condition. split. + apply (Qplus_le_l _ _ (- approximate a ((1 # 2) * e)%Qpos)) in H. simpl in H. ring_simplify in H. ring_simplify. exact H. + apply (Qplus_le_l _ _ (proj1_sig e + approximate b ((1 # 2) * e)%Qpos)) in H0. simpl in H0. ring_simplify in H0. exact H0. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Stability