Theorem afldfracisafld : isaafield afldfrac0. Proof. intros. split. - change ( afldfracapartrel ( @ringunel2 ( commringfrac A (aintdomazerosubmonoid A ) ) ) ( @ringunel1 ( commringfrac A ( aintdomazerosubmonoid A ) ) ) ). unfold afldfracapartrel. set ( aux := @op2 A ( @ringunel2 A ) ( @ringunel2 A ) # @op2 A ( @ringunel1 A ) ( @ringunel2 A ) ). cut (pr1 aux). + intro v. apply v. + unfold aux. rewrite 2! ( @ringrunax2 A ). apply A. - intros a p. apply afldfracmultinv. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.