I am working in constructive mathematics that means without the law of excluded middle. One may also interpret this as working in inuitionistic logic.
Lets assume I have some set $A$ such that I know that $0 \in A$ is decidable. I have another statement $B$. I want to prove that $B \Rightarrow (0 \in A)$. Is the following proof strategy justified in constructive mathematics:
I make a case distinction:
Case 1: $0 \in A$, hence nothing to show.
Case 2: $ 0 \notin A$. Then bla bla bla bla bla $\rightarrow$ contradiction. Hence we must have $0 \in A$.
To be more precise: The contradiction I get in Case 2 is $\neg B$. (this is a contradiction since I assumed $B$).
I am not sure which of the following logical expressions is used in this proof. Either
$B \rightarrow \neg A \rightarrow \neg B \rightarrow A$
$\neg \neg A \rightarrow A$
($\neg A$ is short for $0 \notin A$).