let n, m be Nat; ( n <> 0 implies m / n = ((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0))) )
set fd = divSeq (m,n);
set fm = modSeq (m,n);
assume A1:
n <> 0
; m / n = ((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0)))
hence m / n =
((((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0)) / n
by Th19
.=
(((modSeq (m,n)) . 0) / n) + ((divSeq (m,n)) . 0)
by A1, XCMPLX_1:113
.=
((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0)))
by XCMPLX_1:57
;
verum