Lemma CRisCField : is_CField CRasCRing CRinv.

Lemma CRinv_strext : forall x y x_ y_, CRapart (CRinv x x_) (CRinv y y_) -> CRapart x y.

Definition CRasCField : CField :=
Build_CField CRasCRing CRinv CRisCField CRinv_strext.

Canonical Structure CRasCField.