Lemma padicplusisbinopapartl : isbinopapartl padicapart padicplus. Proof. intros. unfold isbinopapartl. assert ( forall x x' x'' : commringofpadicints, isaprop ( pr1 padicapart ( padicplus x x' ) ( padicplus 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 (padicplus (setquotpr (ringcarryequiv p (isaprimetoneq0 is)) a) (setquotpr (ringcarryequiv p (isaprimetoneq0 is)) b)) (padicplus (setquotpr (ringcarryequiv p (isaprimetoneq0 is)) a) (setquotpr (ringcarryequiv p (isaprimetoneq0 is)) c)) -> pr1 padicapart (setquotpr (ringcarryequiv p (isaprimetoneq0 is)) b) (setquotpr (ringcarryequiv p (isaprimetoneq0 is)) c)). unfold padicplus. rewrite 2! setquotprandpadicplus. rewrite 2! padicapartcomputation. apply padicplusisbinopapart0. 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.