proposition: Lemma setquotprandpadicplus ( a b : fpscommring hz ) : @op1 commringofpadicints ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) a ) ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) b ) = setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) ( a + b ).
proof: Proof. intros. apply commringquotprandop1. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers