Lemma islinvinfldfrac (X : intdom) (is : isdeceq X) (x : commringfrac X (intdomnonzerosubmonoid X)) (ne : x != 0) : (fldfracmultinv0 X is x * x) = 1. Proof. revert x ne. assert (int : ∏ x0, isaprop (x0 != 0 → (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 (setquotpr _ ( (pr1 (fldfracmultinvint X is xa)) * (pr1 xa) ,, @op (intdomnonzerosubmonoid X) (pr2 (fldfracmultinvint X is xa)) (pr2 xa) ) = setquotpr (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (1 ,, 1 ,, nonzeroax X)). apply (weqpathsinsetquot). unfold fldfracmultinvint. simpl. induction (is (pr1 xa) 0 ) as [ e0 | ne0' ]. - induction (nonzeroincommringfrac X (intdomnonzerosubmonoid X) xa ne e0). - apply hinhpr. exists ((1 : X) ,, nonzeroax X). set (x := (pr1 xa) : X). set (aa := pr2 xa). set (a := (pr1 aa) : X). simpl. change (a * x * 1 * 1 = 1 * (x * a) * 1). rewrite (ringcomm2 X a x). repeat rewrite (ringrunax2 X _). rewrite (ringlunax2 X _). apply idpath. Qed.
Require Import UniMath.Algebra.Groups.