proposition: Lemma fpsapartisbinopapartplusr ( R : acommring ) : isbinopapartr ( fpsapart R ) ( @op1 ( fpscommring R ) ).
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers