let a, b be Nat; :: thesis: ( not a,(a + b) ! are_coprime or a = 1 or ( a = 0 & ( b = 0 or b = 1 ) ) )
assume A1: a,(a + b) ! are_coprime ; :: thesis: ( a = 1 or ( a = 0 & ( b = 0 or b = 1 ) ) )

per cases ( a = 0 or a > 0 ) ;

suppose B1: a = 0 ; :: thesis: ( a = 1 or ( a = 0 & ( b = 0 or b = 1 ) ) )

then b <= 1 by A1, Th23;
then b < 1 + 1 by NAT_1:13;
hence ( a = 1 or ( a = 0 & ( b = 0 or b = 1 ) ) ) by B1, NAT_1:23; :: thesis: verum

end;

suppose a > 0 ; :: thesis: ( a = 1 or ( a = 0 & ( b = 0 or b = 1 ) ) )

hence ( a = 1 or ( a = 0 & ( b = 0 or b = 1 ) ) ) by A1, Lm3, NEWTON:49; :: thesis: verum

end;

end;