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