Lemma issymmabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (isl : issymm L) : issymm (abmonoidfracrelint X A L). Proof. intros xa1 xa2. unfold abmonoidfracrelint. simpl. apply hinhfun. intros t2l1. set (c1a := pr1 t2l1). set (l1 := pr2 t2l1). exists (c1a). apply (isl _ _ l1). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.