proposition: Lemma AR_epsilon_sign_dec_pos_rev (x : AR) (k : Z) : cast AQ AR (1 ≪ (1 + k)) ≤ x → AR_epsilon_sign_dec k x ≡ Gt.
proof: Proof. intros E. apply AR_epsilon_sign_dec_Gt. apply (order_reflecting (+ -1 ≪ (1 + k))). transitivity (-1 ≪ k). apply orders.eq_le. rewrite (commutativity _ k), shiftl.shiftl_exp_plus, shiftl.shiftl_1. rewrite rings.plus_mult_distr_r, rings.mult_1_l. rewrite rings.negate_plus_distr, associativity, rings.plus_negate_r. simpl. ring. apply (order_reflecting (cast AQ Q)). rewrite rings.preserves_negate. exact (E ('Pos_shiftl (1 : AQ₊) k)). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring Coq.QArith.Qabs CoRN.stdlib_omissions.Q MathClasses.misc.workaround_tactics CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.util.Qdlog CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.metric2.MetricMorphisms CoRN.reals.fast.CRArith CoRN.reals.fast.CRpower MathClasses.implementations.stdlib_binary_naturals MathClasses.orders.minmax MathClasses.implementations.positive_semiring_elements CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.AQmetric