let a, b, n, m 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 Lm3;
hence (divSeq (m,n)) . b = 0 by A1, Th17; :: thesis: verum