let a, b, m, n be Nat; :: thesis: ( not a < b or (modSeq m,n) . a > (modSeq m,n) . b or (modSeq m,n) . a = 0 )
set fm = modSeq m,n;
assume A1: a < b ; :: thesis: ( (modSeq m,n) . a > (modSeq m,n) . b or (modSeq m,n) . a = 0 )

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

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

end;

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

defpred S₁[ Nat] means ( a < $1 implies (modSeq m,n) . a > (modSeq m,n) . $1 );
A3: S₁[ 0 ] ;
A4: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume A5: S₁[x] ; :: thesis: S₁[x + 1]
assume a < x + 1 ; :: thesis: (modSeq m,n) . a > (modSeq m,n) . (x + 1)
then A6: a <= x by NAT_1:13;

per cases ( a = x or a < x ) by A6, XXREAL_0:1;

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

hence (modSeq m,n) . a > (modSeq m,n) . (x + 1) by A2, Lm3; :: thesis: verum

end;

suppose A7: a < x ; :: thesis: (modSeq m,n) . a > (modSeq m,n) . (x + 1)

thus (modSeq m,n) . a > (modSeq m,n) . (x + 1) :: thesis: verum

proof

per cases ( (modSeq m,n) . x > (modSeq m,n) . (x + 1) or (modSeq m,n) . x = 0 ) by Lm3;

suppose (modSeq m,n) . x > (modSeq m,n) . (x + 1) ; :: thesis: (modSeq m,n) . a > (modSeq m,n) . (x + 1)

hence (modSeq m,n) . a > (modSeq m,n) . (x + 1) by A5, A7, XXREAL_0:2; :: thesis: verum

end;

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

hence (modSeq m,n) . a > (modSeq m,n) . (x + 1) by A2, Th14, NAT_1:11; :: thesis: verum

end;

end;

end;

end;

end;

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A3, A4);
hence ( (modSeq m,n) . a > (modSeq m,n) . b or (modSeq m,n) . a = 0 ) by A1; :: thesis: verum

end;

end;