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

per cases ) . a = 0 or (modSeq (m,n)) . a > 0 ) ;

suppose (modSeq (m,n)) . a = 0 ; :: thesis:

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

end;

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

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

proof

let x be Nat; :: thesis:
assume A4: S₁[x] ; :: thesis:
assume a < x + 1 ; :: thesis:
then A5: a <= x by NAT_1:13;

per cases by A5, XXREAL_0:1;

suppose a = x ; :: thesis:

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

end;

suppose A6: a < x ; :: thesis:

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

proof

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

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

hence (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) by A4, A6, XXREAL_0:2; :: thesis:

end;

suppose (modSeq (m,n)) . x = 0 ; :: thesis:

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

end;

end;

end;

end;

end;

end;

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

end;

end;