proposition: Lemma cc_isCRing : is_CRing cc_cabgroup cc_one cc_mult_op.
proof: Proof. apply Build_is_CRing with cc_cr_mult_associative. exact cc_cr_mult_mon. exact cc_mult_commutes. exact cc_cr_dist. exact cc_cr_non_triv. Qed.
imports: CoRN.reals.NRootIR