Lemma isantisymmnegfldfracgt (X : intdom) (is : isdeceq X) {R : hrel X} (is0 : @isbinophrel X R) (is1 : isringmultgt X R) (is2 : R 1 0) (nc : neqchoice R) (ir : isirrefl R) (isr : isantisymmneg R) : isantisymmneg (fldfracgt X is is0 is1 is2 nc). Proof. intros. assert (int : isantisymmneg (commringfracgt X (ringpossubmonoid X is1 is2) is0 is1 (λ c r, r))). { unfold commringfracgt. apply (isantisymmnegabmonoidfracrel (ringmultabmonoid X) (ringpossubmonoid X is1 is2) (ispartbinopcommringfracgt X (ringpossubmonoid X is1 is2) is0 is1 (λ _ r, r))). apply isr. } intros a b n1 n2. set (e := int _ _ n1 n2). apply (invmaponpathsweq (weqfldfracgt X is is0 is1 is2 nc ir) _ _ e). Qed.
Require Import UniMath.Algebra.Groups.