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