proposition: Lemma CRle_scale : forall (a b : CR) (q : Qpos), (a <= b)%CR <-> (scale (`q) a <= scale (`q) b)%CR.
proof: Proof. assert (forall (a b:CR) (q:Qpos), (a <= b)%CR -> (scale (`q) a <= scale (`q) b)%CR). { intros. intro e. simpl. unfold Cap_raw; simpl. unfold Qscale_modulus. destruct q, x, Qnum. simpl. - exfalso; inversion q. - simpl. rewrite CRle_alt in H. specialize (H ((Qden # p) * ((1#2)*e))%Qpos). simpl in H. setoid_replace (- (2#1) * ((Zpos Qden # p) * ((1 # 2) * ` e)))%Q with (-`e * (Zpos Qden#p))%Q in H by (unfold equiv, stdlib_rationals.Q_eq; ring). apply Qle_shift_div_l in H. 2: reflexivity. apply (Qle_trans _ _ _ H). clear H. unfold Qdiv. setoid_replace (/ (Zpos Qden # p)) with (Zpos p # Qden) by reflexivity. rewrite Qmult_comm. unfold Qminus. rewrite Qmult_plus_distr_r. apply Qplus_le_r. ring_simplify. apply Qle_refl. - exfalso. inversion q. } split. intros. apply H, H0. intros. apply (H _ _ (Qpos_inv q)) in H0. setoid_replace (scale (` (Qpos_inv q)) (scale (` q) a)) with a in H0. setoid_replace (scale (` (Qpos_inv q)) (scale (` q) b)) with b in H0. exact H0. - rewrite <- CRmult_scale, <- CRmult_scale. rewrite <- CRmult_assoc. rewrite CRmult_Qmult. setoid_replace (` (Qpos_inv q) * ` q)%Q with 1%Q. apply CRmult_1_l. simpl. rewrite Qmult_comm, Qmult_inv_r. reflexivity. apply Qpos_nonzero. - rewrite <- CRmult_scale, <- CRmult_scale. rewrite <- CRmult_assoc. rewrite CRmult_Qmult. setoid_replace (` (Qpos_inv q) * ` q)%Q with 1%Q. apply CRmult_1_l. simpl. rewrite Qmult_comm, Qmult_inv_r. reflexivity. apply Qpos_nonzero. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders