Lemma padicintsareintdom ( a b : acommringofpadicints ) : a # 0 -> b # 0 -> a * b # 0. Proof. assert ( forall a b : commringofpadicints, isaprop ( pr1 padicapart a padiczero -> pr1 padicapart b padiczero -> pr1 padicapart ( padictimes a b ) padiczero ) ) as int. { intros. apply impred. intros. apply impred. intros. apply ( pr1 padicapart ). } revert a b. apply ( setquotuniv2prop _ ( fun x y => make_hProp _ ( int x y ) ) ). intros a b. change (pr1 padicapart (setquotpr (carryequiv p (isaprimetoneq0 is)) a) padiczero -> pr1 padicapart (setquotpr (carryequiv p (isaprimetoneq0 is)) b) padiczero -> pr1 padicapart (padictimes (setquotpr (carryequiv p (isaprimetoneq0 is)) a) (setquotpr (carryequiv p (isaprimetoneq0 is)) b)) padiczero). unfold padictimes. rewrite padiczerocomputation. rewrite setquotprandpadictimes. rewrite 3! padicapartcomputation. intros i j. use (hinhuniv _ i). intros i0. destruct i0 as [ i0 i1 ]. use (hinhuniv _ j). intros j0. destruct j0 as [ j0 j1 ]. rewrite carryandzero in i1, j1. change ( ( @ringunel1 ( fpscommring hz ) ) i0 ) with 0%hz in i1. change ( ( @ringunel1 ( fpscommring hz ) ) j0 ) with 0%hz in j1. set ( P := fun x : nat => neq hz ( carry p ( isaprimetoneq0 is ) a x ) 0 ). set ( P' := fun x : nat => neq hz ( carry p ( isaprimetoneq0 is ) b x ) 0 ). assert ( isdecnatprop P ) as isdec1. { intros m. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) a m ) 0%hz ) as [ l | r ]. - apply ii2. intro v. unfold P in v. unfold neq in v. apply v. assumption. - apply ii1. assumption. } assert ( isdecnatprop P' ) as isdec2. { intros m. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b m ) 0%hz ) as [ l | r ]. - apply ii2. intro v. unfold P' in v. unfold neq in v. apply v. assumption. - apply ii1. assumption. } set ( le1 := leastelementprinciple i0 P isdec1 i1 ). set ( le2 := leastelementprinciple j0 P' isdec2 j1 ). use (hinhuniv _ le1). intro k. destruct k as [ k k' ]. use (hinhuniv _ le2). intro o. destruct o as [ o o' ]. apply total2tohexists. split with ( k + o )%nat. assert ( forall m : nat, natlth m k -> carry p ( isaprimetoneq0 is ) a m = 0%hz ) as one. { intros m m0. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) a m ) 0%hz ) as [ left0 | right0 ]. - assumption. - apply fromempty. apply ( ( pr2 k' ) m m0 ). assumption. } assert ( forall m : nat, natlth m o -> carry p ( isaprimetoneq0 is ) b m = 0%hz ) as two. { intros m m0. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b m ) 0%hz ) as [ left0 | right0 ]. - assumption. - apply fromempty. apply ( ( pr2 o' ) m m0 ). assumption. } assert ( neq hz ( carry p ( isaprimetoneq0 is ) a k ) 0%hz × forall m : nat, natlth m k -> ( carry p ( isaprimetoneq0 is ) a m ) = 0%hz ) as three. { split. - apply k'. - assumption. } assert ( neq hz ( carry p ( isaprimetoneq0 is ) b o ) 0%hz × forall m : nat, natlth m o -> ( carry p ( isaprimetoneq0 is ) b m ) = 0%hz ) as four. { split. - apply o'. - assumption. } set ( f := hzfpstimesnonzero ( carry p ( isaprimetoneq0 is ) a ) k three o ( carry p ( isaprimetoneq0 is ) b ) four ). rewrite carryandzero. change ( ( @ringunel1 ( fpscommring hz ) ) ( k + o )%nat ) with 0%hz. rewrite carryandtimes. destruct k. - destruct o. + rewrite <- carryandtimes. intros v. change ( hzremaindermod p ( isaprimetoneq0 is ) ( a 0%nat * b 0%nat ) = 0%hz ) in v. assert hfalse. { use (hinhuniv _ ( hzremaindermodprimeandtimes ( a 0%nat ) ( b 0%nat ) v )). intros t. destruct t as [ t0 | t1 ]. * unfold P in k'. unfold neq in k'. apply ( pr1 k' ). apply t0. * unfold P' in o'. unfold neq in o'. apply ( pr1 o' ). apply t1. } assumption. + intros v. unfold carry at 1 in v. change ( 0 + S o )%nat with ( S o ) in v. change ( hzremaindermod p ( isaprimetoneq0 is ) ( ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) ( S o ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) o ) ) = 0%hz ) in v. change ( 0 + S o )%nat with ( S o) in f. rewrite f in v. change ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) with ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) in v. rewrite ( precarryandzeromult a b 0%nat ( S o ) ) in v. * rewrite hzqrand0q in v. rewrite hzplusr0 in v. assert hfalse. { set (aux := hzremaindermodprimeandtimes ( carry p ( isaprimetoneq0 is ) a 0%nat ) ( carry p ( isaprimetoneq0 is ) b ( S o ) ) v). use (hinhuniv _ aux). intros s. destruct s as [ l | r ]. -- unfold P in k'. unfold neq in k'. apply k'. rewrite hzqrandcarryr. assumption. -- unfold P' in o'. unfold neq in o'. apply o'. rewrite hzqrandcarryr. assumption. } assumption. * apply one. * apply two. * apply natlthnsn. - intros v. unfold carry at 1 in v. change ( hzremaindermod p ( isaprimetoneq0 is ) ( ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) ( S k + o )%nat + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) ( k + o )%nat ) ) = 0%hz ) in v. rewrite f in v. change ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) with ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) in v. rewrite ( precarryandzeromult a b ( S k ) o ) in v. + rewrite hzqrand0q in v. rewrite hzplusr0 in v. assert hfalse. { set (aux := hzremaindermodprimeandtimes ( carry p ( isaprimetoneq0 is ) a ( S k ) ) ( carry p ( isaprimetoneq0 is ) b (o ) ) v). use (hinhuniv _ aux). intros s. destruct s as [ l | r ]. * unfold P in k'. unfold neq in k'. apply k'. rewrite hzqrandcarryr. assumption. * unfold P' in o'. unfold neq in o'. apply o'. rewrite hzqrandcarryr. assumption. } assumption. + apply one. + apply two. + apply natlthnsn. 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.