proposition: Lemma aq_opp : forall (x : AQ), '(-x) = -'x.
proof: Proof. intro x. apply (Qplus_inj_l _ _ ('x)). rewrite Qplus_opp_r. assert ('zero0 = 0%Q) by (apply rings.preserves_0). rewrite <- H5. destruct aq_ring_morphism. destruct semiringmor_plus_mor. destruct monmor_sgmor. rewrite <- preserves_sg_op. destruct sgmor_setmor. apply sm_proper. unfold equiv. destruct aq_ring, ring_group. destruct abgroup_group. apply negate_r. 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