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