proposition: Lemma CReal_isRingExt : ring_eq_ext CReal_plus CReal_mult CReal_opp CRealEq.
proof: Proof. split. - intros x y H z t H0. apply CReal_plus_morph; assumption. - intros x y H z t H0. apply (CRealEq_trans _ (CReal_mult x t)). + apply CReal_mult_proper_l. apply H0. + apply (CRealEq_trans _ (CReal_mult t x)). { apply CReal_mult_comm. } apply (CRealEq_trans _ (CReal_mult t y)). * apply CReal_mult_proper_l. apply H. * apply CReal_mult_comm. - intros x y H. apply (CReal_plus_eq_reg_l x). apply (CRealEq_trans _ (inject_Q 0)). { apply CReal_plus_opp_r. } apply (CRealEq_trans _ (CReal_plus y (CReal_opp y))). + apply CRealEq_sym. apply CReal_plus_opp_r. + apply CReal_plus_proper_r. apply CRealEq_sym. apply H. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra