proposition: Lemma C_field_theory : field_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp Cdiv Cinv eq.
proof: Proof. constructor. constructor. exact Cplus_0_l. exact Cplus_comm. exact Cplus_assoc. exact Cmult_1_l. exact Cmult_comm. exact Cmult_assoc. exact Cmult_plus_distr_r. easy. exact Cplus_opp_r. intros H. injection H. exact R1_neq_R0. easy. apply Cinv_l. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy