Proof in constructive mathematics using decidability. 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$
or
$\neg \neg A \rightarrow A$
($\neg A$ is short for $0 \notin A$).
 A: You know $A\lor\neg A$ and $\neg A\to\neg B$, and you want to prove $B\to A$:
Assume $B$, and we then seek to prove $A$.
Do case analysis on $A\lor\neg A$ (which we already know holds).
In the case $A$ we're done.
In the case $\neg A$, apply $\neg A\to\neg B$ to get $\neg B$. Together with the assumption $B$, this is a contradiction, and by the principle of explosion we're allowed to conclude $A$.
In both cases we could conclude $A$, so $A$, and therefore (discharging the hypothesis) $B\to A$.
All of this is perfectly valid intuitionistcally.
A: By "$0 \in A$" is decidable, we just mean $0 \in A \lor 0 \not \in A$.
Given that assumption, if you can prove $\lnot \lnot (0 \in A)$, you can prove $0 \in A$. As you know $\lnot \lnot (0 \in A)$ is $\lnot (0 \in A) \to \bot$. 
The proof of $0 \in A$ is as follows. 
Case 1: $0 \in A$. Done.
Case 2: $0 \not \in A$, i.e. $\lnot (0 \in A)$. Then, from $\lnot (0 \in A) \to \bot$, we obtain $\bot$. Then, from the contradiction rule $\bot \to 0 \in A$, we have $0 \in A$. 
