Lemma isbinapartrafldfracop2 : isbinopapartr (afldfracapart ) op2. Proof. intros a b c. rewrite ringcomm2. rewrite ( ringcomm2 _ c ). apply isbinapartlafldfracop2. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.