proposition: Lemma AQexp_correct a : 'AQexp a = rational_exp ('a).
proof: Proof. unfold AQexp. case (decide_rel _); intros. rewrite ARtoCR_preserves_inv_pos. rewrite AQexp_neg_correct. rewrite rings.preserves_negate. apply rational_exp_opp. now apply semirings.preserves_nonneg. posed_rewrite <-(rings.preserves_negate (f:=cast AQ Q)). apply (AQexp_inv_pos_bound_correct (a:=-a)). now apply rings.flip_nonneg_negate. apply AQexp_neg_correct. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program MathClasses.misc.workaround_tactics CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qround Coq.QArith.Qabs CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRexp CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.fast.CRpower CoRN.metric2.MetricMorphisms CoRN.reals.faster.ARAlternatingSum MathClasses.interfaces.abstract_algebra MathClasses.orders.minmax MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.reals.faster.ARArith