let m, n be Nat; :: thesis: (divSeq m,n) . 1 = n div ((modSeq m,n) . 0 )
thus (divSeq m,n) . 1 = n div (m mod n) by Def3
.= n div ((modSeq m,n) . 0 ) by Def2 ; :: thesis: verum