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 ) ) )

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