Lemma natbezoutstrong ( m n : nat ) ( i : hzneq 0 ( nattohz n ) ) : ∑ ab : hz × hz, gcd ( nattohz n ) ( nattohz m ) i = pr1 ab * nattohz n + pr2 ab * nattohz m. Proof. revert m n i. set ( E := ( fun m : nat => forall n : nat, forall i : hzneq 0 ( nattohz n ), ∑ ab : hz × hz, gcd ( nattohz n ) ( nattohz m ) i = pr1 ab * nattohz n + pr2 ab * nattohz m ) ). assert ( forall x : nat, E x ) as goal. { apply stronginduction. - unfold E. intros. split with ( make_dirprod 1 0 ). simpl. rewrite nattohzand0. destruct ( gcdand0 ( nattohz n ) i ) as [ left | right ]. + rewrite hzmultl1. rewrite hzplusr0. assumption. + apply fromempty. apply ( isirreflhzlth ( gcd ( nattohz n ) 0 i ) ). apply ( istranshzlth _ 0 _ ). * rewrite right. apply hzgth0andminus. change 0 with ( nattohz 0%nat ). apply nattohzandgth. apply natneq0togth0. use (pr1 (natneq_iff_neq _ _)). intro f. unfold hzneq in i. apply i. rewrite f. apply idpath. * apply gcdpositive. - intros m x y. intros n i. assert ( hzneq 0 ( nattohz m ) ) as p. { intro f. set (aux := pr2 (natneq_iff_neq _ _) x). apply aux. apply pathsinv0. rewrite <- hzabsvalandnattohz. change 0%nat with ( hzabsval ( nattohz 0%nat ) ). apply maponpaths. assumption. } set ( r := hzremaindermod ( nattohz m ) p ( nattohz n ) ). set ( q := hzquotientmod ( nattohz m ) p ( nattohz n ) ). assert ( natlth (hzabsval r ) m ) as p'. { rewrite <- ( hzabsvalandnattohz m ). apply hzabsvalandlth. + exact ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ). + unfold r. rewrite <- ( hzabsvalgeh0 ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ) ). apply nattohzandlth. assert ( natlth ( hzabsval ( hzremaindermod ( nattohz m ) p ( nattohz n ) ) ) ( hzabsval ( nattohz m ) ) ) as ii. { apply hzabsvalandlth. * exact ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ). * assert ( nattohz ( hzabsval ( nattohz m ) ) = nattohz m ) as f. { apply maponpaths. apply hzabsvalandnattohz. } exact ( transportf ( fun x => hzlth ( hzremaindermod ( nattohz m ) p ( nattohz n ) ) x ) f ( hzlthremaindermodmod ( nattohz m ) p ( nattohz n ) ) ). } exact ( transportf ( fun x => natlth ( hzabsval ( hzremaindermod ( nattohz m ) p ( nattohz n ) ) ) x ) ( hzabsvalandnattohz m ) ii ). } set ( c := y ( hzabsval r ) p' m p ). destruct c as [ ab f ]. destruct ab as [ a b ]. simpl in f. split with ( make_dirprod b ( a - b * q ) ). assert ( gcd ( nattohz m ) ( nattohz ( hzabsval r ) ) p = ( gcd ( nattohz n ) ( nattohz m ) i ) ) as g. { apply isantisymmhzleh. + apply ( gcdisgreatest ( nattohz n ) ( nattohz m ) i ). split. * apply ( hzdivlinearcombright ( nattohz n ) ( nattohz m * hzquotientmod ( nattohz m ) p ( nattohz n ) ) r ). -- exact ( hzdivequationmod ( nattohz m ) p ( nattohz n ) ). -- apply hzdivandmultr. apply gcdiscommondiv. -- unfold r. rewrite ( hzabsvalgeh0 ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ) ) . apply ( pr2 ( gcdiscommondiv ( nattohz m ) ( hzremaindermod ( nattohz m ) p ( nattohz n ) ) p ) ). * apply gcdiscommondiv. + apply gcdisgreatest. split. * apply ( pr2 ( gcdiscommondiv _ _ _ ) ). * apply ( hzdivlinearcombleft ( nattohz n ) ( nattohz m * hzquotientmod ( nattohz m ) p ( nattohz n ) ) ( nattohz ( hzabsval r ) ) ). -- unfold r. rewrite ( hzabsvalgeh0 ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ) ). exact ( hzdivequationmod ( nattohz m ) p ( nattohz n ) ). -- apply gcdiscommondiv. -- apply hzdivandmultr. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). } rewrite <- g. rewrite f. simpl. assert ( nattohz ( hzabsval r ) = ( nattohz n - ( q * nattohz m ) ) ) as h. { rewrite ( hzdivequationmod ( nattohz m ) p ( nattohz n ) ). change ( hzquotientmod ( nattohz m ) p ( nattohz n ) ) with q. change ( hzremaindermod ( nattohz m ) p ( nattohz n ) ) with r. rewrite hzpluscomm. change (r + nattohz m * q - q * nattohz m) with ( ( r + nattohz m * q ) + ( - ( q * nattohz m ) ) ). rewrite hzmultcomm. rewrite hzplusassoc. intermediate_path (r + 0). + rewrite hzplusr0. apply hzabsvalgeh0. apply ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ). + apply maponpaths. rewrite <- (hzrminus (q * nattohz m)). apply idpath. } rewrite h. change ( (nattohz n - q * nattohz m) ) with ( (nattohz n + ( - ( q * nattohz m) ) ) ) at 1. rewrite ( ringldistr hz ). rewrite <- hzplusassoc. rewrite ( hzpluscomm ( a * nattohz m ) ). rewrite ringrmultminus. rewrite <- hzmultassoc. rewrite <- ringlmultminus. rewrite hzplusassoc. rewrite <- ( ringrdistr hz ). change (b * nattohz n + (a - b * q) * nattohz m) with ((b * nattohz n)%ring + ((a + - (b * q)%hz) * nattohz m)%ring). apply idpath. } apply goal. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.