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