Definition isdecabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartinvbinophrel A L) (isl : isdecrel L) : isdecrel (abmonoidfracrelint X A L). Proof. intros xa1 xa2. set (x1 := pr1 xa1). set (a1 := pr1 (pr2 xa1)). set (x2 := pr1 xa2). set (a2 := pr1 (pr2 xa2)). assert (int : coprod (L (x1 + a2) (x2 + a1)) (neg (L (x1 + a2) (x2 + a1)))) by apply (isl _ _). induction int as [ l | nl ]. - apply ii1. unfold abmonoidfracrelint. apply hinhpr. exists (unel A). rewrite (runax X _). rewrite (runax X _). apply l. - apply ii2. generalize nl. clear nl. apply negf. unfold abmonoidfracrelint. simpl. apply (@hinhuniv _ (make_hProp _ (pr2 (L _ _)))). intro t2l. induction t2l as [ c0a l ]. simpl. apply ((pr2 is) _ _ _ (pr2 c0a) l). Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.