proposition: Lemma cc_cfield_proof : is_CField cc_cring cc_recip.
proof: Proof. unfold is_CField in |- *. unfold is_inverse in |- *. intro. elim x. intros x1 x2 Hx. split; simpl in |- *; unfold cc_eq in |- *; simpl in |- *; split; rational. Qed.
imports: CoRN.reals.NRootIR