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 ( (modSeq m,n) . a = 0 or (modSeq m,n) . a > 0 ) ;

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

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

end;

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

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

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

A3: (modSeq m,n) . (0 + 1) = n mod (m mod n) by Def2;
(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 A2, A3, NAT_D:1; :: thesis: verum

end;

suppose A4: 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 A4, 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;

end;

end;