Somehow the following fact seems not often taught in proof assistant tutorials, in spite of being incredibly useful: when your current goal is `False`

, you can, while remaining in intuitionistic logic, transform a hypothesis `~~P`

into `P`

, and get a hypothesis `P \/ ~P`

for free.

I have the following tactics to apply this.

- Did I miss some built-in tactics that do this?
- If not: in
`dneg_elim`

, how can I avoid changing the order of hypotheses in the context?

```
Ltac dneg_elim :=
repeat match goal with
| [ H : ~~?P |- False ] => apply H; clear H; intro H
end.
Example dneg_over_implication A B : ~~(A -> B) -> (~~A -> ~~B).
Proof.
intros HAB HA HB. dneg_elim. apply HB, HAB, HA.
Qed.
Lemma double_neg_lem P : ~~(P \/ ~P).
Proof. tauto. Qed.
Tactic Notation "lem" constr(term) "as" simple_intropattern(pat) :=
apply (double_neg_lem term); intros pat.
Example dneg_over_implication_converse A B : (~~A -> ~~B) -> ~~(A -> B).
Proof.
intros H H'. lem A as [HA | HnA].
* lem B as [HB | HnB].
** apply H'. intros _. exact HB.
** apply H, HnB. intro HnA. apply HnA, HA.
* apply H'. intro HA. exfalso. apply HnA, HA.
Qed.
```