Excluded middle equivalents

Definition peirce := forall P Q: Prop,
  ((P->Q)->P)->P.

Definition double_negation_elimination := forall P:Prop,
  ~~P -> P.

Definition de_morgan_not_and_not := forall P Q:Prop,
  ~(~P /\ ~Q) -> P\/Q.

Definition implies_to_or := forall P Q:Prop,
  (P->Q) -> (~P\/Q).

Theorem em_peirce : excluded_middle → peirce.
Proof.
  unfold peirce. intros.
  destruct (H P).
  - assumption.
  - apply H0. intros. exfalso. apply H1. assumption.
Qed.

Theorem em_imp : excluded_middle -> implies_to_or.
Proof.
  intros. unfold implies_to_or.
  intros. destruct (H P).
  - right. apply H0. assumption.
  - left. assumption.
Qed.

Theorem dm_em : de_morgan_not_and_not -> excluded_middle.
Proof.
  unfold de_morgan_not_and_not. unfold excluded_middle.
  intros. apply H. intros [Hnp Hnnp].
  apply Hnnp. assumption.
Qed.

Theorem dm_peirce : de_morgan_not_and_not -> peirce.
Proof.
  intros.
  apply em_peirce. apply dm_em.
  assumption.
Qed.

Theorem dm_imp : de_morgan_not_and_not -> implies_to_or.
Proof.
  intros.
  apply em_imp. apply dm_em.
  assumption.
Qed.

Lemma and_p_p : ∀ P: Prop, P /\ P <-> P.
Proof.
  intros. split; intros.
  - destruct H; assumption.
  - split; assumption.
Qed.

Theorem dm_dne : de_morgan_not_and_not -> double_negation_elimination.
Proof.
  unfold de_morgan_not_and_not. unfold double_negation_elimination.
  intros. assert (P \/ P).
  {
    apply H. rewrite and_p_p. assumption.
  }
  destruct H1; assumption.
Qed.

Theorem em_dm : excluded_middle -> de_morgan_not_and_not.
Proof.
  unfold excluded_middle. unfold de_morgan_not_and_not.
  intros. destruct (H P); destruct (H Q).
  - left. assumption.
  - left. assumption.
  - right. assumption.
  - assert (¬P /\ ¬Q).
    {
      split; assumption.
    }
    exfalso. apply H0. assumption.
Qed.

Theorem dne_dm : double_negation_elimination -> de_morgan_not_and_not.
Proof.
  unfold double_negation_elimination. unfold de_morgan_not_and_not.
  intros. apply (H (P \/ Q)). intros contra.
  apply H0. split.
  - intros contra'. apply contra.
    left. assumption.
  - intros contra'. apply contra.
    right. assumption.
Qed.

Theorem imp_em : implies_to_or -> excluded_middle.
Proof.
  unfold implies_to_or. unfold excluded_middle.
  intros. apply or_commut.
  apply H. intros. assumption.
Qed.

Theorem peirce_em : peirce -> excluded_middle.
Proof.
  unfold peirce. unfold excluded_middle.
  intros. apply (H (P \/ ¬P) (¬P)).
  intros. right. intros contra.
  apply H0. left. assumption. assumption.
Qed.