proposition: Lemma aq_div_above (x y : AQ) (k : Z) : ('x / 'y : Q) ≤ 'app_div_above x y k.
proof: Proof. unfold app_div_above. pose proof (aq_div x y k) as P. apply in_Qball in P. destruct P as [_ P]. rewrite rings.preserves_plus. rewrite aq_shift_correct. now rewrite rings.preserves_1, left_identity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program CoRN.model.totalorder.QposMinMax MathClasses.misc.workaround_tactics CoRN.stdlib_omissions.Q CoRN.util.Qdlog CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.classes.Qclasses CoRN.model.totalorder.QMinMax CoRN.algebra.RSetoid CoRN.metric2.MetricMorphisms MathClasses.orders.minmax MathClasses.orders.dec_fields MathClasses.theory.abs MathClasses.theory.shiftl MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders