let a, b be Element of INT ; :: thesis: ALGO_GCD (a,b) = a gcd b
consider A, B being sequence of NAT such that
P1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & ALGO_GCD (a,b) = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) by defALGOGCD;
set m0 = min* { i where i is Element of NAT : B . i = 0 } ;
X0: { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT by P1, LM5;
then min* { i where i is Element of NAT : B . i = 0 } in { i where i is Element of NAT : B . i = 0 } by NAT_1:def 1;
then P4: ex i being Element of NAT st
( min* { i where i is Element of NAT : B . i = 0 } = i & B . i = 0 ) ;

per cases ( min* { i where i is Element of NAT : B . i = 0 } = 0 or min* { i where i is Element of NAT : B . i = 0 } <> 0 ) ;

suppose C1: min* { i where i is Element of NAT : B . i = 0 } = 0 ; :: thesis: ALGO_GCD (a,b) = a gcd b

thus ALGO_GCD (a,b) = (A . 0) gcd (B . 0) by P4, C1, LM6, P1
.= a gcd b by INT_2:34, P1 ; :: thesis: verum

end;

suppose min* { i where i is Element of NAT : B . i = 0 } <> 0 ; :: thesis: ALGO_GCD (a,b) = a gcd b

then 1 <= min* { i where i is Element of NAT : B . i = 0 } by NAT_1:14;
then 1 - 1 <= (min* { i where i is Element of NAT : B . i = 0 } ) - 1 by XREAL_1:9;
then reconsider m1 = (min* { i where i is Element of NAT : B . i = 0 } ) - 1 as Element of NAT by INT_1:3;
X1: B . m1 <> 0

proof

assume B . m1 = 0 ; :: thesis: contradiction
then X11: m1 in { i where i is Element of NAT : B . i = 0 } ;
(min* { i where i is Element of NAT : B . i = 0 } ) - 1 < (min* { i where i is Element of NAT : B . i = 0 } ) - 0 by XREAL_1:15;
hence contradiction by X11, X0, NAT_1:def 1; :: thesis: verum

end;

then X2: (A . 0) gcd (B . 0) = (A . m1) gcd (B . m1) by P1, LM4;
P3: (A . m1) gcd (B . m1) = (A . (m1 + 1)) gcd (B . (m1 + 1)) by LM3, X1, P1;
(A . (min* { i where i is Element of NAT : B . i = 0 } )) gcd (B . (min* { i where i is Element of NAT : B . i = 0 } )) = ALGO_GCD (a,b) by P1, LM6, P4;
hence ALGO_GCD (a,b) = a gcd b by P3, INT_2:34, X2, P1; :: thesis: verum

end;

end;