Lemma hzmodprimeinv ( p : hz ) ( x : hzneq 0 p ) ( y : isaprime p ) ( a : hz ) ( q : neg ( hzmod p x a 0 ) ) : ∑ v : hz, hzmod p x ( a * v ) 1 × hzmod p x ( v * a ) 1. Proof. intros. split with ( pr2 ( pr1 ( bezoutstrong a p x ) ) ). assert ( 1 = pr1 (pr1 (bezoutstrong a p x)) * p + pr2 (pr1 (bezoutstrong a p x)) * a ) as f'. { assert ( 1 = gcd p a x ) as f''. { apply pathsinv0. apply gcdandprime; assumption. } rewrite f''. apply ( bezoutstrong a p x ). } split. - rewrite f'. simpl. rewrite ( hzmultcomm ( pr1 ( pr1 ( bezoutstrong a p x ) ) ) _ ). rewrite hzremaindermodandmultl. rewrite hzmultcomm. apply idpath. - rewrite f'. simpl. rewrite hzremaindermodandplus. rewrite ( hzremaindermodandtimes p x _ p ). rewrite hzqrandselfr. rewrite hzmultx0. rewrite hzqrand0r. rewrite hzplusl0. rewrite hzremaindermoditerated. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.