Theorem divalgorithmexists ( n m : hz ) ( p : hzneq 0 m ) : ∑ qr : hz × hz, n = m * ( pr1 qr ) + pr2 qr × ( hzleh 0 ( pr2 qr ) × hzlth ( pr2 qr ) ( nattohz ( hzabsval m ) ) ). Proof. intros. destruct ( hzlthorgeh n 0 ) as [ n_neg | n_nonneg ]. - destruct ( hzlthorgeh m 0 ) as [ m_neg | m_nonneg ]. + set ( n' := hzabsval n ). set ( m' := hzabsval m ). assert ( nattohz m' = ( - m ) ) as f. { apply hzabsvallth0. assumption. } assert ( - - n = - ( nattohz n' ) ) as f0. { rewrite <- ( hzabsvallth0 n_neg ). rewrite ( hzabsvallth0 n_neg ). unfold n'. rewrite ( hzabsvallth0 n_neg ). apply idpath. } assert ( hzlth 0 ( nattohz m' ) ) as p'. { assert ( hzlth 0 ( - m ) ) as q. { apply hzlth0andminus. assumption. } rewrite f. assumption. } set ( a := divalgorithmnonneg n' m' p' ). set ( q := pr1 ( pr1 a ) ). set ( r := pr2 ( pr1 a ) ). set ( Q := q + 1 ). set ( R := - m - r ). destruct ( hzlehchoice 0 r ( pr1 ( pr2 ( pr2 a ) ) )) as [ less | equal ]. * split with ( make_dirprod Q R ). split. -- rewrite ( pathsinv0( ringminusminus hz n) ). assert ( - nattohz n' = ( m * Q + R ) ) as f1. { unfold Q. unfold R. rewrite ( pr1 ( ( pr2 a ) ) ). change ( pr1 ( pr1 a ) ) with q. change ( pr2 ( pr1 a ) ) with r. rewrite hzaddinvplus. rewrite <- ( ringlmultminus hz ). rewrite f. rewrite ringminusminus. rewrite ( ringldistr _ q _ _ ). rewrite hzmultr1. change ( ( m * q ) + - r = ( m * q + m ) + ( - m + - r ) ). rewrite hzplusassoc. rewrite <- ( hzplusassoc m _ _ ). change ( m + - m ) with ( m - m ). rewrite hzrminus. rewrite hzplusl0. apply idpath. } exact ( pathscomp0 f0 f1 ). -- split. ++ unfold R. assert ( hzlth r ( - m ) ) as u. { rewrite <- hzabsvalleh0. ** apply ( pr2 ( pr2 ( pr2 ( a ) ) ) ). ** apply hzlthtoleh. assumption. } rewrite <- ( hzlminus m ). change ( pr2 ( make_dirprod Q ( - m - r ) ) ) with ( - m - r ). apply hzlehandplusl. apply hzlthtoleh. rewrite <- ( ringminusminus hz m ). apply hzlthminusswap. assumption. ++ unfold R. unfold m'. rewrite hzabsvalleh0. ** change ( hzlth ( - m + - r ) ( - m ) ). assert ( hzlth ( - m - r ) ( - m + 0 ) ) as u. { apply hzlthandplusl. apply hzgth0andminus. exact less. } assert ( - m + 0 = ( - m ) ) as f' by apply hzplusr0. exact ( transportf ( fun x => hzlth ( - m + - r ) x ) f' u ). ** apply hzlthtoleh. assumption. * split with (make_dirprod q 0 ). split. -- rewrite <- ( ringminusminus hz n ). assert ( - nattohz n' = m * q + 0 ) as f1. { rewrite ( pr1 ( pr2 a ) ). change ( pr1 (pr1 a ) ) with q. change ( pr2 ( pr1 a ) ) with r. rewrite hzplusr0. rewrite ( pathsinv0 equal ). rewrite hzplusr0. assert ( - ( nattohz m' * q ) = - ( nattohz m' ) * q ) as f2. { apply pathsinv0. apply ringlmultminus. } rewrite f2. unfold m'. rewrite hzabsvalleh0. ++ apply ( maponpaths ( fun x => x * q ) ). apply ringminusminus. ++ apply hzlthtoleh. assumption. } exact ( pathscomp0 f0 f1 ). -- split. ++ change ( pr2 ( make_dirprod q 0 ) ) with 0. apply isreflhzleh. ++ rewrite equal. change ( pr2 ( make_dirprod q r ) ) with r. apply ( pr2 ( pr2 ( pr2 a ) ) ). + destruct ( hzgehchoice m 0 m_nonneg ) as [ h | k ]. * assert ( hzlth 0 ( nattohz ( hzabsval m ) ) ) as p'. { rewrite hzabsvalgth0. -- apply h. -- assumption. } set ( a := divalgorithmnonneg ( hzabsval n ) ( hzabsval m ) p' ). set ( q' := pr1 ( pr1 a ) ). set ( r' := pr2 ( pr1 a ) ). assert ( n = - - n ) as f0. { apply pathsinv0. apply ringminusminus. } assert ( - - n = - ( nattohz ( hzabsval n ) ) ) as f1. { apply pathsinv0. apply maponpaths. apply hzabsvalleh0. apply hzlthtoleh. assumption. } destruct ( hzlehchoice 0 r' ( pr1 ( pr2 ( pr2 a ) ) ) ) as [ less | equal ]. -- split with (make_dirprod ( - q' - 1 ) ( m - r' ) ). split. ++ change ( pr1 ( make_dirprod ( - q' - 1 ) ( m - r' ) ) ) with ( - q' - 1 ). change ( pr2 ( make_dirprod ( - q' - 1 ) ( m - r' ) ) ) with ( m - r' ). change ( - q' - 1 ) with ( - q' + ( - 1%hz ) ). rewrite hzldistr. assert ( - nattohz ( hzabsval n ) = ( m * ( - q' ) + m * ( - 1%hz ) ) + ( m - r' ) ) as f2. { rewrite ( pr1 ( pr2 a ) ). change ( pr1 ( pr1 a ) ) with q'. change ( pr2 ( pr1 a ) ) with r'. rewrite hzabsvalgth0. ** rewrite hzaddinvplus. rewrite ( ringrmultminus hz ). rewrite ( hzplusassoc _ ( m * ( - 1%hz ) ) ). apply ( maponpaths ( fun x => - ( m * q' ) + x ) ). assert ( - m + ( m - r' ) = m * ( - 1%hz ) + ( m - r' ) ) as f3. { apply ( maponpaths ( fun x => x + ( m - r' ) ) ). apply pathsinv0. assert ( m * ( - 1%hz ) = - ( m * 1%hz ) ) as f30 by apply ringrmultminus. assert ( - ( m * 1 ) = - m ) as f31. { rewrite hzmultr1. apply idpath. } rewrite f30. assumption. } assert ( - r' = - m + ( m - r' ) ) as f4. { change ( - r' = -m + ( m + - r' ) ). rewrite <- hzplusassoc. rewrite hzlminus, hzplusl0. apply idpath. } rewrite f4. assumption. ** assumption. } rewrite f0, f1. assumption. ++ split. ** change ( pr2 ( make_dirprod ( - q' - 1 ) ( m - r' ) ) ) with ( m - r' ). apply hzlthtoleh. rewrite <- ( hzrminus r' ). apply hzlthandplusr. rewrite <- ( hzabsvalgeh0 m_nonneg ). apply ( pr2 ( pr2 a ) ). ** rewrite ( hzabsvalgeh0 m_nonneg ). assert ( hzlth ( m - r' ) ( m + 0 ) ) as u. { apply hzlthandplusl. apply hzgth0andminus. apply less. } rewrite hzplusr0 in u. assumption. -- split with ( make_dirprod ( - q' ) 0 ). split. ++ change ( pr1 ( make_dirprod ( - q' ) 0 ) ) with ( - q' ). change ( pr2 ( make_dirprod ( - q' ) 0 ) ) with 0. assert ( - nattohz ( hzabsval n ) = m * - q' + 0 ) as f2. { rewrite hzplusr0. rewrite ( pr1 ( pr2 a ) ). change ( pr1 ( pr1 a ) ) with q'. change ( pr2 ( pr1 a ) ) with r'. rewrite <- equal. rewrite hzplusr0. rewrite hzabsvalgeh0. ** apply pathsinv0. apply ringrmultminus. ** assumption. } rewrite f0, f1. assumption. ++ split. ** apply isreflhzleh. ** rewrite equal. apply ( pr2 ( pr2 ( pr2 a ) ) ). * apply fromempty. rewrite k in p. simpl in p. apply p. apply idpath. - set ( choice2 := hzlthorgeh m 0 ). destruct choice2 as [ m_neg | m_nonneg ]. + assert ( hzlth 0 ( nattohz ( hzabsval m ) ) ) as p'. { rewrite hzabsvallth0. * rewrite <- ( ringminusminus hz m ) in m_neg. set ( d:= hzlth0andminus m_neg ). rewrite ringminusminus in d. apply d. * assumption. } set ( a := divalgorithmnonneg ( hzabsval n ) ( hzabsval m ) p' ). set ( q' := pr1 ( pr1 a ) ). set ( r' := pr2 ( pr1 a ) ). split with ( make_dirprod ( - q' ) r' ). split. * rewrite <- hzabsvalgeh0. -- rewrite ( pr1 ( pr2 a ) ). change ( pr1 ( pr1 a ) ) with q'. change ( pr2 ( pr1 a ) ) with r'. change ( pr1 ( make_dirprod ( - q' ) r' ) ) with ( - q' ). change ( pr2 ( make_dirprod ( - q' ) r' ) ) with r'. rewrite hzabsvalleh0. ++ apply ( maponpaths ( fun x => x + r' ) ). assert ( - m * q' = - ( m * q' ) ) as f0 by apply ringlmultminus. assert ( - ( m * q' ) = m * ( - q' ) ) as f1. { apply pathsinv0. apply ringrmultminus. } exact ( pathscomp0 f0 f1 ). ++ apply hzlthtoleh. assumption. -- assumption. * split. -- apply (pr1 ( pr2 ( pr2 a ) ) ). -- apply ( pr2 ( pr2 ( pr2 a ) ) ). + assert ( hzlth 0 ( nattohz ( hzabsval m ) ) ) as p'. { rewrite hzabsvalgeh0. * destruct ( hzneqchoice 0 m ) as [ l | r ]. -- apply p. -- apply fromempty. apply ( isirreflhzgth 0 ). apply ( hzgthgehtrans 0 m 0 ); assumption. -- assumption. * assumption. } set ( a := divalgorithmnonneg ( hzabsval n ) ( hzabsval m ) p' ). set ( q' := pr1 ( pr1 a ) ). set ( r' := pr2 ( pr1 a ) ). split with ( make_dirprod q' r' ). split. -- rewrite <- hzabsvalgeh0. ++ rewrite ( pr1 ( pr2 a ) ). change ( pr1 ( pr1 a ) ) with q'. change ( pr2 ( pr1 a ) ) with r'. change ( pr1 ( make_dirprod q' r' ) ) with q'. change ( pr2 ( make_dirprod q' r' ) ) with r'. rewrite hzabsvalgeh0. ** apply idpath. ** assumption. ++ assumption. -- split. ++ apply ( pr1 ( pr2 ( pr2 a ) ) ). ++ apply ( pr2 ( pr2 ( pr2 a ) ) ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.