Lemma fldfracmultinvintcomp (X : intdom) (is : isdeceq X) : iscomprelrelfun (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (fldfracmultinvint X is). 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. induction (is (pr1 xa1) 0) as [ e1 | ne1 ]. - induction (is (pr1 xa2) 0) as [ e2 | ne2 ]. + now exists ((1 : X) ,, nonzeroax X). + simpl. set (aa0 := pr1 t2). set (a0 := pr1 aa0). assert (e := pr2 t2). change (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 _ _ (!e) (pr2 aa0)). assert (e'' := intdomax2r X _ _ e' (pr2 aa1)). induction (ne2 e''). - induction (is (pr1 xa2) 0) as [ e2 | ne2 ]. + simpl. set (aa0 := pr1 t2). set (a0 := pr1 aa0). assert (e := pr2 t2). change (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)). induction (ne1 e''). + simpl. set (aa0 := pr1 t2). set (a0 := pr1 aa0). assert (e := pr2 t2). exists aa0. change (a1 * x2 * a0 = a2 * x1 * a0). change (x1 * a2 * a0 = x2 * a1 * a0) in e. rewrite (ringcomm2 X a1 x2). rewrite (ringcomm2 X a2 x1). apply (!e). Qed.
Require Import UniMath.Algebra.Groups.