proposition: Lemma fpsapartisbinopapartmultr ( R : acommring ) : isbinopapartr ( fpsapart R ) ( @op2 ( fpsring R ) ).
proof: Proof. intros. intros a b c p. rewrite ( ringcomm2 ( fpscommring R ) ) in p. rewrite ( ringcomm2 ( fpscommring R ) c ) in p. apply ( fpsapartisbinopapartmultl _ a b c ). assumption. Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers