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