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