proposition: Lemma padictimesisbinopapartl : isbinopapartl padicapart padictimes.
proof: Proof. intros. unfold isbinopapartl. assert ( forall x x' x'' : commringofpadicints, isaprop ( pr1 padicapart ( padictimes x x' ) ( padictimes x x'' ) -> ( pr1 padicapart x' x'' ) ) ) as int. { intros. apply impred. intros. apply ( pr1 padicapart ). } apply ( setquotuniv3prop _ ( fun x x' x'' => make_hProp _ ( int x x' x'' ) ) ). intros a b c. change (pr1 padicapart (padictimes (setquotpr (carryequiv p (isaprimetoneq0 is)) a) (setquotpr (carryequiv p (isaprimetoneq0 is)) b)) (padictimes (setquotpr (carryequiv p (isaprimetoneq0 is)) a) (setquotpr (carryequiv p (isaprimetoneq0 is)) c)) -> pr1 padicapart (setquotpr (carryequiv p (isaprimetoneq0 is)) b) (setquotpr (carryequiv p (isaprimetoneq0 is)) c)). unfold padictimes. rewrite 2! setquotprandpadictimes. rewrite 2! padicapartcomputation. intros j. apply ( padictimesisbinopapart0 a b c j ). Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers