proposition: 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: Proof. intros. rewrite 2! ( ringcomm1 ( fpscommring hz ) _ ( carry p ( isaprimetoneq0 is ) a ) ) in x. apply ( padicapartandplusprecarryl a b c n x ). Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers