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