Lemma bezoutstrong ( m n : hz ) ( i : hzneq 0 n ) : ∑ ab : hz × hz, gcd n m i = pr1 ab * n + pr2 ab * m. Proof. intros. assert ( hzneq 0 ( nattohz ( hzabsval n ) ) ) as i'. { intro f. unfold hzneq in i. apply i. destruct ( hzneqchoice 0 n i ) as [ left | right ]. - rewrite hzabsvallth0 in f. + rewrite <- ( ringminusminus hz ). change 0 with ( - - 0 ). apply maponpaths. assumption. + assumption. - rewrite hzabsvalgth0 in f; assumption. } set ( c := (natbezoutstrong (hzabsval m) (hzabsval n) i')). destruct c as [ ab f ]. destruct ab as [ a b ]. simpl in f. assert ( gcd n m i = gcd ( nattohz ( hzabsval n ) ) ( nattohz ( hzabsval m ) ) i' ) as g. { destruct ( hzneqchoice 0 n i ) as [ left_n | right_n ]. - apply isantisymmhzleh. + apply gcdisgreatest. split. * rewrite hzabsvallth0. -- apply hzdivandminus. apply gcdiscommondiv. -- assumption. * destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. -- rewrite hzabsvalgth0. ++ apply ( pr2 ( gcdiscommondiv _ _ _ ) ). ++ assumption. -- rewrite hzabsvalleh0. ++ apply hzdivandminus. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). ++ assumption. + apply gcdisgreatest. split. * apply ( hzdivistrans _ ( nattohz ( hzabsval n ) ) _ ). -- apply gcdiscommondiv. -- rewrite hzabsvallth0. ++ rewrite <- ( ringminusminus hz n ). apply hzdivandminus. rewrite ( ringminusminus hz n ). apply hzdivisrefl. ++ assumption. * apply ( hzdivistrans _ ( nattohz ( hzabsval m ) ) _ ). -- apply ( pr2 ( gcdiscommondiv _ _ _ ) ). -- destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. ++ rewrite hzabsvalgth0. ** apply hzdivisrefl. ** assumption. ++ rewrite hzabsvalleh0. ** rewrite <- ( ringminusminus hz m ). apply hzdivandminus. rewrite ( ringminusminus hz m ). apply hzdivisrefl. ** assumption. - apply isantisymmhzleh. + apply gcdisgreatest. split. * rewrite hzabsvalgth0. -- apply gcdiscommondiv. -- assumption. * apply ( hzdivistrans _ ( nattohz ( hzabsval m ) ) _ ). -- destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. ++ rewrite hzabsvalgth0. ** apply ( pr2 ( gcdiscommondiv _ _ _ ) ). ** assumption. ++ rewrite hzabsvalleh0. ** apply hzdivandminus. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). ** assumption. -- apply hzdivisrefl. + apply gcdisgreatest. split. * apply ( hzdivistrans _ ( nattohz ( hzabsval n ) ) _ ). -- apply gcdiscommondiv. -- rewrite hzabsvalgth0. ++ apply hzdivisrefl. ++ assumption. * apply ( hzdivistrans _ ( nattohz ( hzabsval m ) ) _ ). -- apply ( pr2 ( gcdiscommondiv _ _ _ ) ). -- destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. ++ rewrite hzabsvalgth0. ** apply hzdivisrefl. ** assumption. ++ rewrite hzabsvalleh0. ** rewrite <- ( ringminusminus hz m ). apply hzdivandminus. rewrite ( ringminusminus hz m ). apply hzdivisrefl. ** assumption. } destruct ( hzneqchoice 0 n i ) as [ left_n | right_n ]. - destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. + split with ( make_dirprod ( - a ) b ). simpl. assert ( - a * n + b * m = ( a * nattohz ( hzabsval n ) + b * nattohz ( hzabsval m ) ) ) as l. { rewrite hzabsvallth0. * rewrite hzabsvalgth0. -- rewrite ( ringlmultminus hz ). rewrite <- ( ringrmultminus hz ). apply idpath. -- assumption. * assumption. } rewrite l. rewrite g. exact f. + split with ( make_dirprod ( - a ) ( - b ) ). simpl. rewrite 2! ( ringlmultminus hz ). rewrite <- 2! ( ringrmultminus hz ). rewrite <- hzabsvallth0. * rewrite <- hzabsvalleh0. -- rewrite g. exact f. -- assumption. * assumption. - destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. + split with ( make_dirprod a b ). simpl. rewrite g. rewrite f. rewrite 2! hzabsvalgth0. * apply idpath. * assumption. * assumption. + split with ( make_dirprod a ( - b ) ). rewrite g. rewrite f. simpl. rewrite hzabsvalgth0. * rewrite hzabsvalleh0. -- rewrite ( ringrmultminus hz ). rewrite <- ( ringlmultminus hz ). apply idpath. -- assumption. * assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.