Definition euclidean ( n m : hz ) ( i : hzneq 0 n ) ( p : natleh ( hzabsval m ) ( hzabsval n ) ) : hzgcd n m. Proof. intros. assert ( natneq 0%nat ( hzabsval n ) ) as j. { apply issymm_natneq. apply hzabsvalneq0. intro x. rewrite x in i. simpl in i. apply i. apply idpath. } set ( a := natgcd ( hzabsval m ) ( hzabsval n ) j p ). destruct ( hzlthorgeh 0 n ) as [ left_n | right_n ]. - destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. + rewrite 2! ( hzabsvalgth0 ) in a; assumption. + rewrite hzabsvalgth0 in a. * rewrite hzabsvalleh0 in a. -- rewrite hzgcdandminusr. assumption. -- assumption. * assumption. - destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. + rewrite ( hzabsvalgth0 left_m ) in a. rewrite hzabsvalleh0 in a. * rewrite hzgcdandminusl. assumption. * assumption. + rewrite 2! hzabsvalleh0 in a. * rewrite hzgcdandminusl. rewrite hzgcdandminusr. assumption. * assumption. * assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.