let m, n, a be Nat; :: thesis: ( (divSeq m,n) . (a + 1) = 0 implies (modSeq m,n) . a = 0 )
set fd = divSeq m,n;
set fm = modSeq m,n;
defpred S₁[ Nat] means ( (divSeq m,n) . ($1 + 1) = 0 implies (modSeq m,n) . $1 = 0 );
A1: for b being Nat st S₁[b] holds
S₁[b + 1]

proof

let b be Nat; :: thesis: ( S₁[b] implies S₁[b + 1] )
assume S₁[b] ; :: thesis: S₁[b + 1]
set x = (modSeq m,n) . (b + 1);
assume (divSeq m,n) . ((b + 1) + 1) = 0 ; :: thesis: (modSeq m,n) . (b + 1) = 0
then (divSeq m,n) . (b + (1 + 1)) = 0 ;
then A2: ((modSeq m,n) . b) div ((modSeq m,n) . (b + 1)) = 0 by Def3;
assume A3: (modSeq m,n) . (b + 1) <> 0 ; :: thesis: contradiction
then (modSeq m,n) . b = (((modSeq m,n) . (b + 1)) * (((modSeq m,n) . b) div ((modSeq m,n) . (b + 1)))) + (((modSeq m,n) . b) mod ((modSeq m,n) . (b + 1))) by NAT_D:2;
then A4: (modSeq m,n) . b < (modSeq m,n) . (b + 1) by A2, A3, NAT_D:1;
A5: b + 0 < b + 1 by XREAL_1:8;
then (modSeq m,n) . b <> 0 by A3, Th14;
hence contradiction by A4, A5, Th15; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

set x = m mod n;
assume (divSeq m,n) . (0 + 1) = 0 ; :: thesis: (modSeq m,n) . 0 = 0
then A7: n div ((modSeq m,n) . 0 ) = 0 by Th12;
assume A8: (modSeq m,n) . 0 <> 0 ; :: thesis: contradiction
then m mod n <> 0 by Def2;
then A9: n <> 0 ;
A10: (modSeq m,n) . 0 = m mod n by Def2;
then n = ((m mod n) * (n div (m mod n))) + (n mod (m mod n)) by A8, NAT_D:2;
then n < m mod n by A7, A10, A8, NAT_D:1;
hence contradiction by A9, NAT_D:1; :: thesis: verum

end;

for b being Nat holds S₁[b] from NAT_1:sch 2(A6, A1);
hence ( (divSeq m,n) . (a + 1) = 0 implies (modSeq m,n) . a = 0 ) ; :: thesis: verum