proposition: Lemma islinvinfldfrac (X : intdom) (is : isdeceq X) (x : commringfrac X (intdomnonzerosubmonoid X)) (ne : x != 0) : paths ((fldfracmultinv0 X is x) * x) 1.
proof: Proof. revert x ne. assert (int : ∏ x0, isaprop (x0 != 0 -> paths ((fldfracmultinv0 X is x0) * x0) 1)). { intro x0. apply impred. intro. apply (setproperty (commringfrac X (intdomnonzerosubmonoid X)) (fldfracmultinv0 X is x0 * x0) _). } apply (setquotunivprop _ (λ x0, make_hProp _ (int x0))). simpl. intros xa ne. change (paths (setquotpr (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (make_dirprod ((pr1 (fldfracmultinvint X is xa)) * (pr1 xa)) (@op (intdomnonzerosubmonoid X) (pr2 (fldfracmultinvint X is xa)) (pr2 xa)))) (setquotpr _ (make_dirprod 1 (tpair _ 1 (nonzeroax X))))). apply (weqpathsinsetquot). unfold fldfracmultinvint. simpl. destruct (is (pr1 xa) 0 ) as [ e0 | ne0' ]. - destruct (nonzeroincommringfrac X (intdomnonzerosubmonoid X) xa ne e0). - apply hinhpr. split with (tpair (λ a, a != 0) 1 (nonzeroax X)). set (x := (pr1 xa) : X). set (aa := pr2 xa). set (a := (pr1 aa) : X). simpl. change (paths (a * x * 1 * 1) (1 * (x * a) * 1)). rewrite (ringcomm2 X a x). repeat rewrite (ringrunax2 X _). rewrite (ringlunax2 X _). apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings