Definition natgcd ( m n : nat ) : ( natneq 0%nat n ) -> ( natleh m n ) -> ( hzgcd ( nattohz n ) ( nattohz m ) ). Proof. revert m n. set ( E := ( fun m : nat => forall n : nat, ( natneq 0%nat n ) -> ( natleh m n ) -> (hzgcd ( nattohz n ) ( nattohz m ) ) ) ). assert ( forall x : nat, E x ) as goal. { apply stronginduction. - intros n x0 x1. split with ( nattohz n ). split. + unfold iscommonhzdiv. split. * unfold hzdiv. intros P s. apply s. unfold hzdiv0. split with 1. rewrite hzmultr1. apply idpath. * unfold hzdiv. intros P s. apply s. unfold hzdiv0. split with 0. rewrite hzmultx0. rewrite nattohzand0. apply idpath. + intros l t. destruct t as [ t0 t1 ]. destruct ( hzgthorleh l 0 ) as [ left | right ]. * rewrite <- hzabsvalgth0. -- apply nattohzandleh. unfold hzdiv in t0. use (hinhuniv _ t0). intro t2. destruct t2 as [ k t2 ]. unfold hzdiv0 in t2. assert ( natleh ( hzabsval l ) n ⨿ ( n = 0%nat ) ) as C. { apply ( natdivleh ( hzabsval l ) n ( hzabsval k ) ). apply ( invmaponpathsincl _ isinclnattohz ). rewrite nattohzandmult. rewrite 2! hzabsvalgeh0. ++ assumption. ++ assert ( hzgeh ( l * k ) ( l * 0 ) ) as i. { rewrite hzmultx0. rewrite t2. change 0 with ( nattohz 0%nat ). apply nattohzandgeh. apply x1. } apply ( hzgehandmultlinv _ _ l ); assumption. ++ apply hzgthtogeh. assumption. } destruct C as [ C0 | C1 ]. ++ assumption. ++ apply fromempty. rewrite C1 in x0. apply x0. -- assumption. * apply ( istranshzleh _ 0 _ ). { assumption. } change 0 with ( nattohz 0%nat ). apply nattohzandleh. assumption. - intros m p q. intros n i j. assert ( hzlth 0 ( nattohz m ) ) as p'. { change 0 with ( nattohz 0%nat ). apply nattohzandlth. apply natneq0togth0. apply p. } set ( a := divalgorithmnonneg n m p' ). destruct a as [ qr a ]. destruct qr as [ quot rem ]. destruct a as [ f a ]. destruct a as [ a b ]. simpl in b. simpl in f. assert ( natlth ( hzabsval rem ) m ) as p''. { rewrite <- ( hzabsvalandnattohz m ). apply nattohzandlthinv. rewrite 2! hzabsvalgeh0. + assumption. + apply hzgthtogeh. apply ( hzgthgehtrans _ rem ); assumption. + assumption. } assert ( natleh ( hzabsval rem ) n ) as i''. { apply natlthtoleh. apply nattohzandlthinv. rewrite hzabsvalgeh0. + apply ( hzlthlehtrans _ ( nattohz m ) _ ). * assumption. * apply nattohzandleh. assumption. + assumption. } assert ( natneq 0%nat m ) as p'''. { apply issymm_natneq. assumption. } destruct ( q ( hzabsval rem ) p'' m p''' ( natlthtoleh _ _ p'' ) ) as [ rr c ]. destruct c as [ c0 c1 ]. split with rr. split. + split. * apply ( hzdivlinearcombright ( nattohz n ) ( nattohz m * quot ) rem rr f ). -- apply hzdivandmultr. exact ( pr1 c0 ). -- rewrite hzabsvalgeh0 in c0. ++ exact ( pr2 c0 ). ++ assumption. * exact ( pr1 c0 ). + intros l o. apply c1. split. * exact ( pr2 o ). * rewrite hzabsvalgeh0. -- apply ( hzdivlinearcombleft ( nattohz n ) ( nattohz m * quot ) rem l f ). ++ exact ( pr1 o ). ++ apply hzdivandmultr. exact ( pr2 o ). -- assumption. } assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.