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