let a, b, n, m be Nat; ( 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
; ( 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
; (divSeq (m,n)) . b = 0
then
(divSeq (m,n)) . (a + 1) = 0
by Lm3;
hence
(divSeq (m,n)) . b = 0
by A1, Th17; verum