theorem Th12: :: REAL_3:12
for n, m being Nat holds (divSeq (m,n)) . 1 = n div ((modSeq (m,n)) . 0)