Lemma hzremaindermodprimeandtimes ( a b : hz ) ( x : hzremaindermod p ( isaprimetoneq0 is ) ( a * b ) = 0 ) : hzremaindermod p ( isaprimetoneq0 is ) a = 0 ∨ hzremaindermod p ( isaprimetoneq0 is ) b = 0. Proof. intros. assert ( hzdiv p ( a * b ) ) as i. { intros P i'. apply i'. split with ( hzquotientmod p ( isaprimetoneq0 is ) ( a * b ) ). unfold hzdiv0. apply pathsinv0. rewrite <- ( hzplusr0 (p * hzquotientmod p (isaprimetoneq0 is) (a * b)%ring) )%hz. change (a * b = (p * hzquotientmod p (isaprimetoneq0 is) (a * b)%ring + 0)%ring). rewrite <- x. change (p * hzquotientmod p (isaprimetoneq0 is) (a * b) + hzremaindermod p (isaprimetoneq0 is) a * b) with (p * hzquotientmod p (isaprimetoneq0 is) (a * b)%ring + ( hzremaindermod p (isaprimetoneq0 is) a * b )%ring )%hz. apply ( hzdivequationmod p ( isaprimetoneq0 is ) ( a * b ) ). } use (hinhuniv _ ( primeandtimes a b i )). intro t. destruct t as [ t0 | t1 ]. - use (hinhuniv _ t0). intros k. destruct k as [ k k' ]. intros Q j. apply j. apply ii1. apply pathsinv0. apply ( hzqrtestr p ( isaprimetoneq0 is ) a k ). split. + rewrite hzplusr0. unfold hzdiv0 in k'. rewrite k'. apply idpath. + split. * apply isreflhzleh. * rewrite hzabsvalgth0. -- apply ( istranshzlth _ 1 _ ). ++ apply hzlthnsn. ++ apply is. -- apply ( istranshzlth _ 1 _ ). ++ apply hzlthnsn. ++ apply is. - use (hinhuniv _ t1). intros k. destruct k as [ k k' ]. intros Q j. apply j. apply ii2. apply pathsinv0. apply ( hzqrtestr p ( isaprimetoneq0 is ) b k ). split. + rewrite hzplusr0. unfold hzdiv0 in k'. rewrite k'. apply idpath. + split. * apply isreflhzleh. * rewrite hzabsvalgth0. -- apply ( istranshzlth _ 1 _ ). ++ apply hzlthnsn. ++ apply is. -- apply ( istranshzlth _ 1 _ ). ++ apply hzlthnsn. ++ apply is. 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.