let m, n, a be Nat; :: thesis: ( (modSeq m,n) . a > (modSeq m,n) . (a + 1) or (modSeq m,n) . a = 0 )
set fm = modSeq m,n;

per cases ( a = 0 or a = 1 or a > 1 ) by NAT_1:26;

suppose A1: a = 0 ; :: thesis: ( (modSeq m,n) . a > (modSeq m,n) . (a + 1) or (modSeq m,n) . a = 0 )

( (modSeq m,n) . (0 + 1) = n mod (m mod n) & (modSeq m,n) . 0 = m mod n ) by Def2;
hence ( (modSeq m,n) . a > (modSeq m,n) . (a + 1) or (modSeq m,n) . a = 0 ) by A1, NAT_D:1; :: thesis: verum

end;

suppose A2: a = 1 ; :: thesis: ( (modSeq m,n) . a > (modSeq m,n) . (a + 1) or (modSeq m,n) . a = 0 )

(modSeq m,n) . (0 + 2) = ((modSeq m,n) . 0 ) mod ((modSeq m,n) . (0 + 1)) by Def2;
hence ( (modSeq m,n) . a > (modSeq m,n) . (a + 1) or (modSeq m,n) . a = 0 ) by A2, NAT_D:1; :: thesis: verum

end;

suppose a > 1 ; :: thesis: ( (modSeq m,n) . a > (modSeq m,n) . (a + 1) or (modSeq m,n) . a = 0 )

then reconsider a1 = a - 1 as Nat by Lm1;
(modSeq m,n) . (a + 1) = (modSeq m,n) . (a1 + (1 + 1))
.= ((modSeq m,n) . a1) mod ((modSeq m,n) . (a1 + 1)) by Def2 ;
hence ( (modSeq m,n) . a > (modSeq m,n) . (a + 1) or (modSeq m,n) . a = 0 ) by NAT_D:1; :: thesis: verum

end;

end;