Definition ahzmod ( p : hz ) ( y : isaprime p ) : afld. Proof. intros. split with ( acommring_hzmod p ( isaprimetoneq0 y ) ). split. - simpl. intro f. apply ( isirreflhzlth 0 ). assert ( hzlth 0 1 ) as i by apply hzlthnsn. change ( 1%ring ) with ( setquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) 1%hz ) in f. change ( 0%ring ) with ( setquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) 0%hz ). assert ( hzmodisringeqrel p ( isaprimetoneq0 y ) 1%hz 0%hz ) as o. { apply ( weqpathsinsetquot ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) 1%hz 0%hz ). assumption. } unfold hzmodisringeqrel in o. simpl in o. assert ( hzremaindermod p ( isaprimetoneq0 y ) 0 = 0 ) as o'. { rewrite hzqrand0r. apply idpath. } rewrite o' in o. assert ( hzremaindermod p ( isaprimetoneq0 y ) 1 = 1 ) as o''. { assert ( hzlth 1 p ) as v by apply y. rewrite hzqrand1r. apply idpath. } rewrite o'' in o. assert ( hzlth 0 1 ) as o''' by apply hzlthnsn. rewrite o in o'''. assumption. - assert ( forall x0 : acommring_hzmod p ( isaprimetoneq0 y ), isaprop ( ( x0 # 0)%ring -> multinvpair ( acommring_hzmod p ( isaprimetoneq0 y ) ) x0 ) ) as int. { intro a. apply impred. intro q. apply isapropmultinvpair. } apply ( setquotunivprop _ ( fun x0 => make_hProp _ ( int x0 ) ) ). intro a. simpl. intro q. assert ( neg ( hzmod p ( isaprimetoneq0 y ) a 0 ) ) as q'. { intro g. unfold hzmod in g. simpl in g. apply q. change ( 0%ring ) with ( setquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) 0%hz ). apply ( iscompsetquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) ). apply g. } split with ( setquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) ( pr1 ( hzmodprimeinv p ( isaprimetoneq0 y ) y a q' ) ) ). split. + simpl. rewrite ( quotientringsumdecom hz ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) ). change 1%multmonoid with ( setquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) 1%hz ). apply ( iscompsetquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) ). simpl. change (pr2 (pr1 (bezoutstrong a p ( isaprimetoneq0 y ))) * a)%ring with (pr2 (pr1 (bezoutstrong a p ( isaprimetoneq0 y ))) * a)%hz. exact ( ( pr2 ( pr2 ( hzmodprimeinv p ( isaprimetoneq0 y ) y a q' ) ) )). + simpl. rewrite ( quotientringsumdecom hz ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) ). change 1%multmonoid with ( setquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) 1%hz ). apply ( iscompsetquotpr ( hzmodisringeqrel p ( isaprimetoneq0 y ) ) ). change (a * pr2 (pr1 (bezoutstrong a p ( isaprimetoneq0 y ))))%ring with (a * pr2 (pr1 (bezoutstrong a p ( isaprimetoneq0 y ))))%hz. exact ( ( pr1 ( pr2 ( hzmodprimeinv p ( isaprimetoneq0 y ) y a q' ) ) )). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.