let
a
,
b
be
Nat
;
:: thesis:
(
a
is
even
&
a
gcd
b
=
1 implies
a
gcd
(
2
*
b
)
=
2 )
assume
A1
: (
a
is
even
&
a
gcd
b
=
1 ) ;
:: thesis:
a
gcd
(
2
*
b
)
=
2
a
,
b
are_coprime
by
A1
;
then
a
gcd
(
b
*
2
)
=
a
gcd
2
by
INT_6:19
;
hence
a
gcd
(
2
*
b
)
=
2
by
A1
,
NEWTON:49
;
:: thesis:
verum