for a, b being Nat holds
( not a,(a + b) ! are_coprime or a = 1 or ( a = 0 & ( b = 0 or b = 1 ) ) )