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