let a, b, m, n be Nat; :: thesis: ( a < b & (modSeq m,n) . a = 0 implies (divSeq m,n) . b = 0 )
set fd = divSeq m,n;
set fm = modSeq m,n;
assume a < b ; :: thesis: ( not (modSeq m,n) . a = 0 or (divSeq m,n) . b = 0 )
then A1: a + 1 <= b by NAT_1:13;
assume (modSeq m,n) . a = 0 ; :: thesis: (divSeq m,n) . b = 0
then (divSeq m,n) . (a + 1) = 0 by Lm4;
hence (divSeq m,n) . b = 0 by A1, Th17; :: thesis: verum