Lemma padicapartandplusprecarryr ( a b c : fpscommring hz ) ( n : nat ) ( x : neq _ ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) b + carry p ( isaprimetoneq0 is ) a ) n ) ( ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) c + carry p ( isaprimetoneq0 is ) a ) ) n ) ) : padicapart0 b c. Proof. intros. rewrite 2! ( ringcomm1 ( fpscommring hz ) _ ( carry p ( isaprimetoneq0 is ) a ) ) in x. apply ( padicapartandplusprecarryl a b c n x ). 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.