Lemma padictimesisbinopapart0 ( 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' ]. destruct n. - apply total2tohexists. split with 0%nat. intros j. unfold neq in n'. apply n'. rewrite carryandtimes. rewrite ( carryandtimes p ( isaprimetoneq0 is ) a c ). change ( hzremaindermod p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a 0%nat * carry p ( isaprimetoneq0 is ) b 0%nat ) = hzremaindermod p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a 0%nat * carry p ( isaprimetoneq0 is ) c 0%nat ) ). rewrite j. apply idpath. - set ( Q := ( fun o : nat => make_hProp ( carry p ( isaprimetoneq0 is ) b o = carry p ( isaprimetoneq0 is ) c o ) ( isasethz _ _ ) ) ). assert ( isdecnatprop Q ) as isdec'. { intro o. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b o ) ( carry p ( isaprimetoneq0 is ) c o ) ) as [ l | r ]. + apply ii1. assumption. + apply ii2. assumption. } destruct ( isdecisbndqdec Q isdec'( S n ) ) as [ l | r ]. + apply ( padicapartandtimesprecarryl a b c n ). intros j. apply fromempty. unfold neq in n'. apply n'. rewrite carryandtimes. rewrite ( carryandtimes p ( isaprimetoneq0 is ) a c ). change ( hzremaindermod p ( isaprimetoneq0 is ) ( natsummation0 ( S n ) ( fun x : nat => carry p ( isaprimetoneq0 is ) a x * carry p ( isaprimetoneq0 is ) b ( sub ( S n ) x ) ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) n ) ) = ( hzremaindermod p ( isaprimetoneq0 is ) ( natsummation0 ( S n ) ( fun x : nat => carry p ( isaprimetoneq0 is ) a x * carry p ( isaprimetoneq0 is ) c ( sub ( S n ) x ) ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) c ) n ) ) ) ). rewrite j. assert ( natsummation0 ( S n ) (fun x0 : nat => carry p (isaprimetoneq0 is) a x0 * carry p (isaprimetoneq0 is) b ( sub ( S n ) x0)) = natsummation0 ( S n ) (fun x0 : nat => carry p (isaprimetoneq0 is) a x0 * carry p (isaprimetoneq0 is) c ( sub ( S n ) x0)) ) as f. { apply natsummationpathsupperfixed. intros m y. rewrite ( l ( sub ( S n ) m ) ). * apply idpath. * apply minusleh. } rewrite f. apply idpath. + use (hinhuniv _ r). intros k. destruct k as [ k k' ]. apply total2tohexists. split with k. apply k'. 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.