proposition: Lemma padicplusisbinopapartl : isbinopapartl padicapart padicplus.
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers