proposition: Lemma inject_Q_AR_0 : inject_Q_AR (0#1) = 0.
proof: Proof. intros e1 e2. simpl. destruct aq_dense_embedding. simpl in dense_inverse. rewrite Qplus_0_r. apply (@ball_weak_le Q_as_MetricSpace (`e1) (`e1+`e2)). apply (Qle_trans _ (`e1 + 0)). rewrite Qplus_0_r. apply Qle_refl. apply Qplus_le_r, Qpos_nonneg. simpl. unfold cast. destruct aq_ring_morphism, semiringmor_plus_mor. rewrite preserves_mon_unit. apply dense_inverse. 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