Lemma weqfldfracgtintcomp_f (X : intdom) {R : hrel X} (is0 : @isbinophrel X R) (is1 : isringmultgt X R) (is2 : R 1 0) (nc : neqchoice R) : iscomprelrelfun (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (eqrelcommringfrac X (ringpossubmonoid X is1 is2)) (weqfldfracgtint_f X is0 is1 is2 nc). Proof. intros. intros xa1 xa2. simpl. set (x1 := pr1 xa1). set (aa1 := pr2 xa1). set (a1 := pr1 aa1). set (x2 := pr1 xa2). set (aa2 := pr2 xa2). set (a2 := pr1 aa2). apply hinhfun. intro t2. exists ((1 : X) ,, is2). set (aa0 := pr1 t2). set (a0 := pr1 aa0). assert (e := pr2 t2). change (x1 * a2 * a0 = x2 * a1 * a0) in e. unfold weqfldfracgtint_f. induction (nc (pr1 (pr2 xa1)) 0 (pr2 (pr2 xa1))) as [ g1 | l1 ]. - induction (nc (pr1 (pr2 xa2)) 0 (pr2 (pr2 xa2))) as [ g2 | l2 ]. + simpl. rewrite (ringrunax2 X _). rewrite (ringrunax2 X _). apply (intdomrcan X _ _ _ (pr2 aa0) e). + simpl. rewrite (ringrunax2 X _). rewrite (ringrunax2 X _). rewrite (ringrmultminus X _ _). rewrite (ringlmultminus X _ _). apply (maponpaths (λ x : X, - x)). apply (intdomrcan X _ _ _ (pr2 aa0) e). - induction (nc (pr1 (pr2 xa2)) 0 (pr2 (pr2 xa2))) as [ g2 | l2 ]. + simpl. rewrite (ringrunax2 X _). rewrite (ringrunax2 X _). rewrite (ringrmultminus X _ _). rewrite (ringlmultminus X _ _). apply (maponpaths (λ x : X, - x)). apply (intdomrcan X _ _ _ (pr2 aa0) e). + simpl. rewrite (ringrunax2 X _). rewrite (ringrunax2 X _). rewrite (ringrmultminus X _ _). rewrite (ringlmultminus X _ _). rewrite (ringrmultminus X _ _). rewrite (ringlmultminus X _ _). apply (maponpaths (λ x : X, - - x)). apply (intdomrcan X _ _ _ (pr2 aa0) e). Qed.
Require Import UniMath.Algebra.Groups.