proposition: Lemma padictimesisbinopapartr : isbinopapartr padicapart padictimes.
proof: Proof. intros. unfold isbinopapartr. intros a b c. unfold padictimes. rewrite ( @ringcomm2 commringofpadicints b a ). rewrite ( @ringcomm2 commringofpadicints c a ). apply padictimesisbinopapartl. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers