proposition: Lemma isapropisafield (X : commring) : isaprop (isafield X).
proof: Proof. use isofhleveltotal2. - apply propproperty. - intros H. use impred. intros x. use isapropcoprod. + use isapropinvpair. + use setproperty. + intros H' e. use H. use (pathscomp0 _ (@multx0_is_l X (@op1 X) (@op2 X) (dirprod_pr1 (ringop1axs X)) (ringop2axs X) (ringdistraxs X) (pr1 H'))). use (pathscomp0 _ (maponpaths (λ y : X , op2 (pr1 H') y) e)). exact (! dirprod_pr1 (pr2 H')). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings