proposition: Lemma padicapartandplusprecarryl ( 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: 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'' ]. destruct 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. - apply total2tohexists. split with ( S k ). intro i. apply ( k'' k ). + apply natlthnsn. + intro j. unfold P in k'. unfold neq in k'. apply k'. change ( 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 ( 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 ) ) ). rewrite i. rewrite j. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers