Lemma padicplusisbinopapart0 ( a b c : fpscommring hz ) ( u : padicapart0 ( a + b ) ( a + c ) ) : padicapart0 b c. Proof. intros. use (hinhuniv _ u). intros n. destruct n as [ n n' ]. set ( P := fun x : nat => neq hz ( carry p ( isaprimetoneq0 is ) ( a + b) x) ( carry p ( isaprimetoneq0 is ) ( a + c) x) ). assert ( isdecnatprop P ) as isdec. { intros m. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) ( a + b) m) ( carry p ( isaprimetoneq0 is ) ( a + c) m) ) as [ l | r ]. - apply ii2. intros j. unfold P in j. unfold neq in j. apply j. assumption. - apply ii1. assumption. } set ( le := leastelementprinciple n P isdec n'). use (hinhuniv _ le). intro k. destruct k as [ k k' ]. destruct k' as [ k' k'' ]. destruct k. - apply total2tohexists. split with 0%nat. intros j. unfold P in k'. unfold neq in k'. apply k'. unfold carry. unfold precarry. change ( ( a + b ) 0%nat ) with ( a 0%nat + b 0%nat ). change ( ( a + c ) 0%nat ) with ( a 0%nat + c 0%nat ). unfold carry in j. unfold precarry in j. rewrite hzremaindermodandplus. rewrite j. rewrite <- hzremaindermodandplus. apply idpath. - destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b ( S k ) ) ( carry p ( isaprimetoneq0 is ) c ( S k ) ) ) as [ l | r ]. + apply ( padicapartandplusprecarryl a b c k ). intros j. unfold P in k'. unfold neq in k'. apply k'. rewrite carryandplus. unfold carry at 1. change (hzremaindermod p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a ( S k ) + carry p ( isaprimetoneq0 is ) b ( S k ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) b ) k ) ) = carry p ( isaprimetoneq0 is ) ( a + c ) ( S k ) ). rewrite l. rewrite j. rewrite ( carryandplus p ( isaprimetoneq0 is ) a c ). unfold carry at 5. change ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) c ) ( S k ) ) with ( carry p ( isaprimetoneq0 is ) a ( S k ) + carry p ( isaprimetoneq0 is ) c ( S k ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) c ) k ) ). apply idpath. + apply total2tohexists. split with ( S k ). assumption. 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.