proposition: Lemma divalgorithmnonneg ( n : nat ) ( m : nat ) ( p : hzlth 0 ( nattohz m ) ) : ∑ qr : hz × hz, nattohz n = ( ( nattohz m ) * ( pr1 qr ) ) + ( pr2 qr ) × ( hzleh 0 ( pr2 qr ) × hzlth ( pr2 qr ) ( nattohz m ) ).
proof: Proof. revert p. induction n. - intros. split with ( make_dirprod 0 0 ). split. + simpl. rewrite ( ringrunax1 hz ). rewrite ( ringmultx0 hz ). rewrite nattohzand0. change ( 0 = 0%hz ). apply idpath. + split. * apply isreflhzleh. * assumption. - intro p. set ( q' := pr1 ( pr1 ( IHn p ) ) ). set ( r' := pr2 ( pr1 ( IHn p ) ) ). set ( f := pr1 ( pr2 ( IHn p ) ) ). assert ( hzleh ( r' + 1 ) ( nattohz m ) ) as p'. { assert ( hzlth ( r' + 1 ) ( nattohz m + 1 ) ) as p''. { apply hzlthandplusr. apply ( pr2 ( pr2 ( pr2 ( IHn p ) ) ) ). } apply hzlthsntoleh. assumption. } set ( choice := hzlehchoice ( r' + 1 ) ( nattohz m ) p' ). destruct choice as [ k | h ]. + split with ( make_dirprod q' ( r' + 1 ) ). split. * rewrite (nattohzandS _ ). rewrite hzpluscomm. rewrite f. change ( nattohz m * q' + r' + 1 = nattohz m * q' + ( r' + 1 ) ). apply ringassoc1. * split. -- apply ( istranshzleh 0 r' ( r' + 1 ) ). ++ apply ( pr2 ( pr2 ( IHn p ) ) ). ++ apply hzlthtoleh. apply hzlthnsn. -- assumption. + split with ( make_dirprod ( q' + 1 ) 0 ). split. * rewrite ( nattohzandS _ ). rewrite hzpluscomm. rewrite f. change ( nattohz m * q' + r' + 1 = nattohz m * ( q' + 1 ) + 0 ). rewrite hzplusassoc. rewrite h. rewrite ( ringldistr _ q' _ ). rewrite ringrunax2. rewrite hzplusr0. apply idpath. * split. -- apply isreflhzleh. -- assumption. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble