Lemma fpsapartisbinopapartplusr ( R : acommring ) : isbinopapartr ( fpsapart R ) ( @op1 ( fpscommring R ) ). Proof. intros. intros a b c p. rewrite ( ringcomm1 ( fpscommring R ) ) in p. rewrite ( ringcomm1 ( fpscommring R ) c ) in p. apply ( fpsapartisbinopapartplusl _ a b c ). assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.