Lemma gcdanddiv ( n m : hz ) ( i : hzneq 0 n ) ( p : hzdiv n m ) : ( gcd n m i = n ) ⨿ ( gcd n m i = - n ). Proof. intros. destruct ( hzneqchoice 0 n i ) as [ left | right ]. - apply ii2. apply isantisymmhzleh. + use (hinhuniv _ ( hzdivhzabsval ( gcd n m i ) n ( pr1 ( gcdiscommondiv n m i ) ) )). intro c'. destruct c' as [ c0 | c1 ]. * rewrite <- hzabsvalgeh0. -- rewrite <- hzabsvallth0. ++ apply nattohzandleh. assumption. ++ assumption. -- apply hzgthtogeh. apply ( gcdpositive n m i ). * apply fromempty. assert ( n = 0 ) as f. { rewrite hzabsvaleq0. -- apply idpath. -- assumption. } unfold hzneq in i. apply i. apply pathsinv0. assumption. + apply gcdisgreatest. apply commonhzdivsignswap. split. * apply hzdivisrefl. * assumption. - apply ii1. apply isantisymmhzleh. + use (hinhuniv _ ( hzdivhzabsval ( gcd n m i ) n ( pr1 ( gcdiscommondiv n m i ) ) )). intro c'. destruct c' as [ c0 | c1 ]. * rewrite <- hzabsvalgth0. -- assert ( n = nattohz ( hzabsval n ) ) as f. { apply pathsinv0. apply hzabsvalgth0. assumption. } assert ( hzleh ( nattohz ( hzabsval ( gcd n m i ) ) ) ( nattohz ( hzabsval n ) ) ) as j. { apply nattohzandleh. assumption. } exact ( transportf ( fun x => hzleh ( nattohz ( hzabsval ( gcd n m i ) ) ) x ) ( pathsinv0 f ) j ). -- apply gcdpositive. * apply fromempty. unfold hzneq in i. apply i. apply pathsinv0. rewrite hzabsvaleq0. -- apply idpath. -- assumption. + apply ( gcdisgreatest n m i ). split. * apply hzdivisrefl. * assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.