proposition: Lemma Qscale_modulus_pos (a e: Qpos): exists P, Qscale_modulus (proj1_sig a) e ≡ Qpos2QposInf (exist (Qlt 0) (/ proj1_sig a * proj1_sig e)%Q P).
proof: Proof. revert a. intros [[[] ad] P]; try discriminate. simpl. unfold Qpos_inv, Qpos_mult. eauto. 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