Lemma istotalabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (isl : istotal L) : istotal (abmonoidfracrelint X A L). 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. exists (unel A). rewrite (runax X _). rewrite (runax X _). apply l. intro l. apply hinhpr. exists (unel A). rewrite (runax X _). rewrite (runax X _). apply l. Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.