Definition isdecabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isinvbinophrel L) (isl : isdecrel L) : isdecrel (abgrdiffrelint X L). Proof. intros xa1 xa2. set (x1 := pr1 xa1). set (a1 := pr2 xa1). set (x2 := pr1 xa2). set (a2 := 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 abgrdiffrelint. apply hinhpr. exists 0. rewrite (runax X _). rewrite (runax X _). apply l. - apply ii2. generalize nl. clear nl. apply negf. unfold abgrdiffrelint. simpl. apply (@hinhuniv _ (make_hProp _ (pr2 (L _ _)))). intro t2l. induction t2l as [ c0a l ]. simpl. apply ((pr2 is) _ _ c0a l). Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.