Equivalence between middle excluded law and double negation elimination in Heyting algebra It's well-know that in intuitionistic logic, middle excluded law and double negation elimination are equivalent.
For example, in Johnstone - Topo theory, I read that, in a Heyting algebra, $p\vee\neg p=\top$ holds if and only if $\neg\neg p=p$ for all elements $p$.
In particular, it's easy to prove $(p\vee\neg p)\leq(\neg\neg p\Rightarrow p)$:
for we have $p\Rightarrow(\neg\neg p\Rightarrow p)=(p\wedge\neg\neg p)\Rightarrow p=\top$ and $\neg p\Rightarrow (\neg\neg p\Rightarrow p)=(\neg p\wedge\neg\neg p)\Rightarrow\perp\Rightarrow p=\top$, consequently, $(p\vee\neg p)\Rightarrow(\neg\neg p\Rightarrow p)=\top$.
On the other hand, I can't prove inverse inclusion $(\neg\neg p\Rightarrow p)\leq (p\vee\neg p)$.
Thus my question is:

In a Heyting algebra, does $(\neg\neg p\Rightarrow p)\leq (p\vee\neg p)$ holds?

The proof that I founded here don't satisfy me because it proves only the inference rule $(\neg\neg p\Rightarrow p)\vdash (p\vee\neg p)$.
 A: As you apparently already know, if $((\neg\neg p)\implies p)=\top$ for all $p$ in some Heyting algebra, then also $(p\lor\neg p)=\top$ for all $p$ in that Heyting algebra. Nevertheless, if $((\neg\neg p)\implies p)=\top$ for a particular $p$ in a Heyting algebra, it does not follow that $(p\lor\neg p)=\top$ for that same $p$.
For example, $((\neg\neg p)\implies p)=\top$ is true whenever $p$ is of the form $\neg q$, because $(\neg\neg\neg q)\implies(\neg q)$ is intuitionistically valid.  But it is not intuitionistically valid that $(\neg q)\lor(\neg\neg q)$.
A simple explicit counterexample is the Heyting algebra of open subsets of the real line. Let $p$ be the open half-line $(0,\infty)$. The negation $\neg p$, i.e., the largest open set disjoint from $p$, is the open half-line $(-\infty,0)$, and $\neg\neg p$ equals $p$. So $((\neg\neg p)\implies p)=\top$, but $(p\lor\neg p)=\mathbb R-\{0\}\neq\top$.
A: We cannot prove in intuitionsitc logic :


$\vdash (\lnot \lnot p \Rightarrow p) \Leftrightarrow (p \lor \lnot p)$.



As you said, we can prove :

$(p \lor \lnot p) \Rightarrow (\lnot \lnot p \Rightarrow p)$.

For the other "direction", we can prove only a "negative version" of the theorem.
References are to Intuitionistic logic and to Heyting algebra.
1) $(\lnot \lnot p \Rightarrow p) \le (\lnot p \Rightarrow \lnot \lnot \lnot p)$ --- the law : $a \Rightarrow b \le \lnot b \Rightarrow \lnot a$ is intuitionistically valid
2) $(\lnot p \Rightarrow \lnot \lnot \lnot p) \le (\lnot p \Rightarrow \lnot p)$ --- the law : $\lnot \lnot \lnot a = \lnot a$ is intuitionistically valid
3) $= \lnot (\lnot p \land p)$ --- the law : $(a \Rightarrow \lnot b) = \lnot (a \land b)$ is intuitionistically valid
4) $= \lnot \lnot (\lnot \lnot p \lor \lnot p)$ --- weak De Morgan's law : $\lnot (x \land y) = \lnot \lnot (\lnot x \lor \lnot y)$ holds in HA
Conclusion :
$(\lnot \lnot p \Rightarrow p) \le \lnot \lnot (\lnot \lnot p \lor \lnot p)$
i.e.


$\vdash (\lnot \lnot p \Rightarrow p) \Rightarrow \lnot \lnot (\lnot \lnot p \lor \lnot p)$.



Addendum
Here we have a proof with sequent calculus LK of :

$\vdash (\lnot \lnot P \supset P) \supset (P \lor \lnot P)$.

i) left thread :

$${P \Rightarrow P \over P \Rightarrow P \lor \lnot P } \, \lor\text{-right} \,$$

ii) right thread :

$${P \Rightarrow P \over P, \lnot P \Rightarrow  } \, \lnot\text{-left}$$
$${\over \lnot P \Rightarrow \lnot P } \, \lnot\text{-right}$$
$${\over \lnot P \Rightarrow P \lor \lnot P } \, \lor\text{-right}$$ 
$${\over \Rightarrow P \lor \lnot P, \lnot \lnot P} \, \lnot\text{-right}$$ 

Note. The last step is not intuitionistically valid because violates the restriction that :

a sequent in LJ is of the form $\Gamma \Rightarrow \Delta$, where $\Delta$ consists of at most one formula. 

iii) conclusion
Now we "join" the two threads :


$${P \Rightarrow P \lor \lnot P \quad \quad \Rightarrow P \lor \lnot P, \lnot \lnot P \over \lnot \lnot P \supset P \Rightarrow P \lor \lnot P }\, \supset\text{-left}$$
$${\over \Rightarrow (\lnot \lnot P \supset P) \supset (P \lor \lnot P) }\, \supset\text{-right}$$


Regarding the impossibility of finding a proof of it in LJ, see Jan von Plato, Elements of Logical Reasoning (2013), page 82 :

Given $A \lor \lnot A$, if $\lnot \lnot A$ is assumed, $A$ follows and therefore the implication $\lnot \lnot A \supset A$ follows from $A \lor \lnot A$. An easy proof search in intuitionistic sequent calculus gives a formal derivation for :

$A \lor \lnot A \supset (\lnot \lnot A \supset A)$.

A similar proof search for the converse fails, for there is no derivation of :

$(\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.

[...]
The overall situation is that if $\vdash \lnot \lnot A \supset A$, then $\vdash A \lor \lnot A$, but not $\vdash (\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.

