Lemma isantisymmnegabmonoidfracrel (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (isl : isantisymmneg L) : isantisymmneg (abmonoidfracrel X A is). Proof. intros. assert (int : ∏ x1 x2, isaprop (neg (abmonoidfracrel X A is x1 x2) → neg (abmonoidfracrel X A is x2 x1) → x1 = x2)). { intros x1 x2. apply impred. intro. apply impred. intro. apply (isasetsetquot _ x1 x2). } unfold isantisymmneg. apply (setquotuniv2prop _ (λ x1 x2, make_hProp _ (int x1 x2))). intros xa1 xa2. intros r r'. apply (weqpathsinsetquot _). generalize r r'. clear r r'. change (neg (abmonoidfracrelint X A L xa1 xa2) → neg (abmonoidfracrelint X A L xa2 xa1) → (eqrelabmonoidfrac X A xa1 xa2)). intros nr12 nr21. set (nr12' := neghexisttoforallneg _ nr12 (unel A)). set (nr21' := neghexisttoforallneg _ nr21 (unel A)). set (int' := isl _ _ nr12' nr21'). simpl. apply hinhpr. exists (unel A). apply int'. Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.