Lemma isrinvinfldfrac (X : intdom) (is : isdeceq X) (x : commringfrac X (intdomnonzerosubmonoid X)) (ne : x != 0) : x * fldfracmultinv0 X is x = 1. Proof. intros. rewrite (ringcomm2 _ _ _). apply islinvinfldfrac. apply ne. Defined.
Require Import UniMath.Algebra.Groups.