proposition: Lemma Qscale_modulus_elim : forall (P:QposInf -> Type) (x:Q) (e:Qpos), (x==0 -> P QposInfinity)%Q -> (forall y:Qpos, QAbsSmall (proj1_sig e/proj1_sig y)%Q (x)%Q -> (P y)) -> P (Qscale_modulus x e).
proof: Proof. intros P [xn xd] e H1. cut (forall xn:positive, (forall y : Qpos, QAbsSmall (proj1_sig e/proj1_sig y)%Q (Z.pos xn#xd)%Q -> P y) -> P (Qscale_modulus (Z.pos xn # xd) e)). intros H H2. destruct xn as [|xn|xn]. apply H1. constructor. apply H. assumption. apply H. intros y Hy. apply H2. change (Zneg xn # xd)%Q with (-(Zpos xn # xd))%Q. apply QAbsSmall_opp, Hy. clear xn H1. intros xn H2. simpl. apply H2. simpl. unfold QAbsSmall. setoid_replace (` e / ((Zpos xd # xn) * ` e)) with (Zpos xn # xd). split. 2: apply Qle_refl. apply (Qplus_le_l _ _ (Zpos xn # xd)). ring_simplify. apply (Qpos_nonneg ((2#1)*(xn#xd))). unfold Qdiv. rewrite Qinv_mult_distr. rewrite <- (Qmult_comm (/ `e)), Qmult_assoc. rewrite Qmult_inv_r, Qmult_1_l. reflexivity. apply Qpos_nonzero. 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