proposition: Lemma isbinapartrafldfracop1 : isbinopapartr afldfracapart op1.
proof: Proof. intros a b c. rewrite ringcomm1. rewrite ( ringcomm1 _ c ). apply isbinapartlafldfracop1. Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields