proposition: Lemma padicplusisbinopapartr : isbinopapartr padicapart padicplus.
proof: Proof. intros. unfold isbinopapartr. intros a b c. unfold padicplus. rewrite ( @ringcomm1 commringofpadicints b a ). rewrite ( @ringcomm1 commringofpadicints c a ). apply padicplusisbinopapartl. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers