proposition: Lemma istotalabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (isl : istotal L) : istotal (abmonoidfracrelint X A L).
proof: Proof. unfold istotal. intros x1 x2. unfold abmonoidfracrelint. set (int := isl (pr1 x1 + pr1 (pr2 x2)) (pr1 x2 + pr1 (pr2 x1))). generalize int. clear int. simpl. apply hinhfun. apply coprodf. intro l. apply hinhpr. split with (unel A). rewrite (runax X _). rewrite (runax X _). apply l. intro l. apply hinhpr. split with (unel A). rewrite (runax X _). rewrite (runax X _). apply l. Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders