Lemma isrinv_CFinv : ∏ (x : X) (Hx0 : x ≠ 0), x * (CFinv x Hx0) = 1. Proof. exact (isrinv_CCDRinv (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)). Qed.
Require Import UniMath.MoreFoundations.Tactics.