proposition: Lemma fldfracmultinvintcomp (X : intdom) (is : isdeceq X) : iscomprelrelfun (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (fldfracmultinvint X is).
proof: Proof. intros. intros xa1 xa2. set (x1 := pr1 xa1). set (aa1 := pr2 xa1). set (a1 := pr1 aa1). set (x2 := pr1 xa2). set (aa2 := pr2 xa2). set (a2 := pr1 aa2). simpl. apply hinhfun. intro t2. unfold fldfracmultinvint. destruct (is (pr1 xa1) 0) as [ e1 | ne1 ]. - destruct (is (pr1 xa2) 0) as [ e2 | ne2 ]. + simpl. split with (tpair (λ x, x != 0) 1 (nonzeroax X)). apply idpath. + simpl. set (aa0 := pr1 t2). set (a0 := pr1 aa0). assert (e := pr2 t2). change (paths (x1 * a2 * a0) (x2 * a1 * a0)) in e. change (x1 = 0) in e1. rewrite e1 in e. rewrite (ringmult0x X _) in e. rewrite (ringmult0x X _) in e. assert (e' := intdomax2r X _ _ (pathsinv0 e) (pr2 aa0)). assert (e'' := intdomax2r X _ _ e' (pr2 aa1)). destruct (ne2 e''). - destruct (is (pr1 xa2) 0) as [ e2 | ne2 ]. + simpl. set (aa0 := pr1 t2). set (a0 := pr1 aa0). assert (e := pr2 t2). change (paths (x1 * a2 * a0) (x2 * a1 * a0)) in e. change (x2 = 0) in e2. rewrite e2 in e. rewrite (ringmult0x X _) in e. rewrite (ringmult0x X _) in e. assert (e' := intdomax2r X _ _ e (pr2 aa0)). assert (e'' := intdomax2r X _ _ e' (pr2 aa2)). destruct (ne1 e''). + simpl. set (aa0 := pr1 t2). set (a0 := pr1 aa0). assert (e := pr2 t2). split with aa0. change (paths (a1 * x2 * a0) (a2 * x1 * a0)). change (paths (x1 * a2 * a0) (x2 * a1 * a0)) in e. rewrite (ringcomm2 X a1 x2). rewrite (ringcomm2 X a2 x1). apply (pathsinv0 e). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings