let a, b, m, n be Nat; :: thesis: ( a <= b & (modSeq m,n) . a = 0 implies (modSeq m,n) . b = 0 )
set fm = modSeq m,n;
assume that
A1: a <= b and
A2: (modSeq m,n) . a = 0 ; :: thesis: (modSeq m,n) . b = 0
defpred S₁[ Nat] means ( a < $1 implies (modSeq m,n) . $1 = 0 );
A3: S₁[ 0 ] ;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

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

suppose A7: k = 0 ; :: thesis: (modSeq m,n) . (k + 1) = 0

then A8: a = 0 by A6;
thus (modSeq m,n) . (k + 1) = n mod ((modSeq m,n) . 0 ) by A7, Th13
.= 0 by A2, A8 ; :: thesis: verum

end;

suppose A9: k = 1 ; :: thesis: (modSeq m,n) . (k + 1) = 0

then A10: ( a = 0 or a = 1 ) by A6, NAT_1:26;
2 = 2 + 0 ;
hence (modSeq m,n) . (k + 1) = ((modSeq m,n) . 0 ) mod ((modSeq m,n) . (0 + 1)) by A9, Def2
.= 0 by A2, A10 ;
:: thesis: verum

end;

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

then reconsider k1 = k - 1 as Nat by Lm1;

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

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

thus (modSeq m,n) . (k + 1) = (modSeq m,n) . (k1 + 2)
.= ((modSeq m,n) . k1) mod ((modSeq m,n) . (k1 + 1)) by Def2
.= 0 by A2, A11 ; :: thesis: verum

end;

suppose A12: a < k ; :: thesis: (modSeq m,n) . (k + 1) = 0

thus (modSeq m,n) . (k + 1) = (modSeq m,n) . (k1 + 2)
.= ((modSeq m,n) . k1) mod ((modSeq m,n) . (k1 + 1)) by Def2
.= 0 by A5, A12 ; :: thesis: verum

end;

end;

end;

end;

end;

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