Lemma padictimesisbinopapartl : isbinopapartl padicapart padictimes. 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.
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.