Lemma primeandtimes ( a b : hz ) ( x : hzdiv p ( a * b ) ) : hzdiv p a ∨ hzdiv p b. Proof. intros. use (hinhuniv _ ( primedivorcoprime a )). intros j. intros P i. apply i. destruct j as [ j0 | j1 ]. - apply ii1. assumption. - apply ii2. use (hinhuniv _ x). intro u. destruct u as [ k u ]. unfold hzdiv0 in u. set ( cd := bezoutstrong a p ( isaprimetoneq0 is ) ). destruct cd as [ cd f ]. destruct cd as [ c d ]. rewrite j1 in f. simpl in f. assert ( b = ( b * c + d * k ) * p ) as g. { assert ( b = b * 1 ) as g0. { rewrite hzmultr1. apply idpath. } rewrite g0. rewrite ( ringrdistr hz ( b * 1 * c ) ( d * k ) p ). assert ( b * ( c * p + d * a ) = b * 1 * c * p + d * k * p ) as h. { rewrite ( ringldistr hz ( c * p ) ( d * a ) b ). rewrite hzmultr1. rewrite 2! ( @ringassoc2 hz ). rewrite ( @ringcomm2 hz k p ). change ( p * k )%hz with ( p * k )%ring in u. rewrite u. rewrite ( @ringcomm2 hz b ( d * a ) ). rewrite ( @ringassoc2 hz ). apply idpath. } rewrite <- h. rewrite f. apply idpath. } intros Q uu. apply uu. split with ( b * c + d * k ). rewrite ( @ringcomm2 hz _ p ) in g. unfold hzdiv0. apply pathsinv0. 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.