proposition: Lemma CReal_isRing : ring_theory (inject_Q 0) (inject_Q 1) CReal_plus CReal_mult CReal_minus CReal_opp CRealEq.
proof: Proof. intros. split. - apply CReal_plus_0_l. - apply CReal_plus_comm. - intros x y z. symmetry. apply CReal_plus_assoc. - apply CReal_mult_1_l. - apply CReal_mult_comm. - intros x y z. symmetry. apply CReal_mult_assoc. - intros x y z. rewrite <- (CReal_mult_comm z). rewrite CReal_mult_plus_distr_l. apply (CRealEq_trans _ (CReal_plus (CReal_mult x z) (CReal_mult z y))). + apply CReal_plus_proper_r. apply CReal_mult_comm. + apply CReal_plus_proper_l. apply CReal_mult_comm. - intros x y. apply CRealEq_refl. - apply CReal_plus_opp_r. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra