proposition: Lemma isantisymmnegabmonoidfracrel (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (isl : isantisymmneg L) : isantisymmneg (abmonoidfracrel X A is).
proof: 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. split with (unel A). apply int'. Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders