let a, b be Integer; :: thesis: for A, B being sequence of NAT st A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Nat st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))

let A, B be sequence of NAT; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Nat st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )

assume A1: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; :: thesis: for i being Nat st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))

let i be Nat; :: thesis: ( B . i <> 0 implies (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
assume A2: B . i <> 0 ; :: thesis: (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
set k = (A . i) gcd (B . i);
A4: B . (i + 1) = (A . i) mod (B . i) by A1;
A3: A . (i + 1) = B . i by A1;
then A5: (A . i) gcd (B . i) divides A . (i + 1) by INT_2:def 2;
A6: (A . i) gcd (B . i) divides B . (i + 1)
proof
A7: B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by ;
A8: (A . i) gcd (B . i) divides A . i by INT_2:def 2;
A9: (A . i) gcd (B . i) divides B . i by INT_2:def 2;
ex s being Integer st A . i = ((A . i) gcd (B . i)) * s by A8;
then consider s, t being Integer such that
A11: B . (i + 1) = (((A . i) gcd (B . i)) * s) - (((A . i) div (B . i)) * (((A . i) gcd (B . i)) * t)) by A7, A9;
B . (i + 1) = (s - (((A . i) div (B . i)) * t)) * ((A . i) gcd (B . i)) by A11;
hence (A . i) gcd (B . i) divides B . (i + 1) ; :: thesis: verum
end;
for m being Integer st m divides A . (i + 1) & m divides B . (i + 1) holds
m divides (A . i) gcd (B . i)
proof
let m be Integer; :: thesis: ( m divides A . (i + 1) & m divides B . (i + 1) implies m divides (A . i) gcd (B . i) )
assume A12: ( m divides A . (i + 1) & m divides B . (i + 1) ) ; :: thesis: m divides (A . i) gcd (B . i)
then A13: m divides B . i by A1;
A14: m divides A . i
proof
B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by ;
then A15: A . i = (B . (i + 1)) + (((A . i) div (B . i)) * (B . i)) ;
A16: ex s being Integer st B . i = m * s by A13;
A17: ex t being Integer st B . (i + 1) = m * t by A12;
consider s, t being Integer such that
A18: A . i = (m * s) + (((A . i) div (B . i)) * (m * t)) by ;
A . i = m * (s + (((A . i) div (B . i)) * t)) by A18;
hence m divides A . i ; :: thesis: verum
end;
thus m divides (A . i) gcd (B . i) by ; :: thesis: verum
end;
hence (A . (i + 1)) gcd (B . (i + 1)) = (A . i) gcd (B . i) by ; :: thesis: verum