proposition: Lemma divalgorithm ( n m : hz ) ( p : hzneq 0 m ) : iscontr ( ∑ qr : hz × hz, n = ( m * ( pr1 qr ) ) + ( pr2 qr ) × ( hzleh 0 ( pr2 qr ) × hzlth ( pr2 qr ) ( nattohz ( hzabsval m ) ) ) ).
proof: Proof. intros. split with ( divalgorithmexists n m p ). intro t. destruct t as [ qr' t' ]. destruct qr' as [ q' r' ]. simpl in t'. destruct t' as [ f' p2p2t ]. destruct p2p2t as [ p1p2p2t p2p2p2t ]. destruct divalgorithmexists as [ qr v ]. destruct qr as [ q r ]. destruct v as [ f p2p2dae ]. destruct p2p2dae as [ p1p2p2dae p2p2p2dae ]. simpl in f. simpl in p1p2p2dae. simpl in p2p2p2dae. assert ( r' = r ) as h. { assert ( m * ( q - q' ) = ( r' - r ) ) as h0. { change ( q - q' ) with ( q + - q' ). rewrite hzldistr. rewrite <- ( hzplusr0 ( r' - r ) ). rewrite <- ( hzrminus ( m * q' ) ). change ( r' - r ) with ( r' + ( - r ) ). rewrite ( hzplusassoc r' ). change ( ( m * q' ) - ( m * q' ) ) with ( ( m * q' ) + ( - ( m * q' ) ) ). rewrite <- ( hzplusassoc ( - r ) ). rewrite ( hzpluscomm ( -r ) ). rewrite <- ( hzplusassoc r' ). rewrite <- ( hzplusassoc r' ). rewrite ( hzpluscomm r' ). rewrite <- f'. rewrite f. rewrite ( hzplusassoc ( m * q ) ). change ( r + - r ) with ( r - r ). rewrite hzrminus. rewrite hzplusr0. rewrite ( ringrmultminus hz ). change ( m * q + - ( m * q' ) ) with ( ( m * q + - ( m * q' ) )%ring ). apply idpath. } assert ( natleh ( hzabsval m ) ( hzabsval ( r' - r ) ) ∨ hzabsval ( r' - r ) = 0%nat ) as v. { apply hzdivhzabsval. intro P. intro s. apply s. split with ( q - q' ). unfold hzdiv0. assumption. } assert ( isaprop ( r' = r ) ) as P by apply isasethz. apply ( v ( make_hProp ( r' = r ) P ) ). intro s. destruct s as [ left | right ]. - assert ( hzlth ( nattohz ( hzabsval ( r' - r ) ) ) ( nattohz ( hzabsval m ) ) ) as u. { destruct ( hzgthorleh r' r ) as [ greater | lesseq ]. + assert ( hzlth 0 ( r' - r ) ) as e. { rewrite <- ( hzrminus r ). apply hzlthandplusr. assumption. } rewrite hzabsvalgth0. * apply hzlthminus. -- exact p2p2p2t. -- exact p2p2p2dae. -- exact p1p2p2dae. * apply e. + destruct ( hzlehchoice r' r lesseq ) as [ less | equal ]. * rewrite hzabsvalandminuspos. -- rewrite hzabsvalgth0. ++ apply hzlthminus. ** exact p2p2p2dae. ** exact p2p2p2t. ** exact p1p2p2t. ++ apply hzlthminusequiv. assumption. -- exact p1p2p2t. -- exact p1p2p2dae. * rewrite equal. rewrite hzrminus. rewrite hzabsval0. rewrite nattohzand0. assert (hzabsval m ≠ 0). { apply hzabsvalneq0. intro Q. rewrite Q in p. simpl in p. apply p. apply idpath. } apply lemmas.hzabsvalneq0. assumption. } apply fromempty. apply ( isirreflhzlth ( nattohz ( hzabsval m ) ) ). apply ( hzlehlthtrans _ ( nattohz ( hzabsval ( r' - r ) ) ) _ ). + apply nattohzandleh. assumption. + assumption. - assert ( r' = r ) as i. { assert ( r' - r = 0 ) as i0. { apply hzabsvaleq0. assumption. } rewrite <- ( hzplusl0 r ). rewrite <- ( hzplusr0 r' ). assert ( r' + ( r - r ) = ( 0 + r ) ) as i00. { change ( r - r ) with ( r + - r ). rewrite ( hzpluscomm _ ( - r ) ). rewrite <- hzplusassoc. apply ( maponpaths ( fun x : _ => x + r ) ). apply i0. } exact ( transportf ( fun x : _ => ( r' + x = ( 0 + r ) ) ) ( ( hzrminus r ) ) i00 ). } apply i. } assert ( q' = q ) as g. { rewrite h in f'. rewrite f in f'. apply ( hzmultlcan q' q m ). - intro i. rewrite i in p. simpl in p. apply p. apply idpath. - apply ( hzplusrcan ( m * q' ) ( m * q ) r ). apply pathsinv0. apply f'. } assert ( make_dirprod q' r' = ( make_dirprod q r ) ) as j by (apply pathsdirprod; assumption). apply ( total2_paths2_f j ). assert ( iscontr ( n = m * q + r × ( hzleh 0 r × hzlth r ( nattohz ( hzabsval m ) ) ) ) ) as contract. { change iscontr with ( isofhlevel 0 ). apply isofhleveldirprod. - split with f. intro t. apply isasethz. - apply isofhleveldirprod. + split with p1p2p2dae. intro t. apply hzleh. + split with p2p2p2dae. intro t. apply hzlth. } apply proofirrelevancecontr. assumption. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble