Theorem euclideanalgorithm ( n m : hz ) ( i : hzneq 0 n ) : iscontr ( hzgcd n m ). Proof. intros. destruct ( natgthorleh ( hzabsval m ) ( hzabsval n ) ) as [ left | right ]. - assert ( hzneq 0 m ) as i'. { intro f. apply ( negnatlthn0 ( hzabsval n ) ). rewrite <- f in left. rewrite hzabsval0 in left. assumption. } set ( a := euclidean m n i' ( natlthtoleh _ _ left ) ). rewrite hzgcdsymm in a. split with a. intro. apply isaprophzgcd. - split with ( euclidean n m i right ). intro. apply isaprophzgcd. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.