let a, n, m 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 Def2;
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:6;
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 Def1;
then A9: n <> 0 ;
A10: (modSeq (m,n)) . 0 = m mod n by Def1;
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