let n, m be Nat; :: thesis: ( 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 ; :: thesis: 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:114
.= ((divSeq m,n) . 0 ) + (1 / (n / ((modSeq m,n) . 0 ))) by XCMPLX_1:57 ;
:: thesis: verum