Library decidable

Require Import Decidable.

Lemma not_and_iff : ∀ A B : Prop, decidable A → ¬ (A ∧ B) ↔ ¬ A ∨ ¬ B.
Proof.
  split; intros.
  - destruct H. right. intros contra. apply H0. split; assumption.
    left; assumption.
  - intros contra. destruct contra.
    destruct H0; contradiction.
Qed.

Lemma not_or_iff : ∀ A B : Prop, ¬ (A ∨ B) ↔ ¬ A ∧ ¬ B.
Proof.
  split; intros.
  - split; intros contra; apply H; [left | right]; assumption.
  - destruct H. intros contra. destruct contra; contradiction.
Qed.

Lemma and_or_distr_l : ∀ P Q R,
  (P ∨ Q) ∧ R ↔ P ∧ R ∨ Q ∧ R.
Proof.
  split; intros.
  - do 2 destruct H.
    + left; split; assumption.
    + right; split; assumption.
  - do 2 destruct H; split; try assumption.
    + left; assumption.
    + right; assumption.
Qed.

Lemma dec_is_decidable : ∀ P, {P}+{¬P} → decidable P.
Proof.
  intros. destruct H; [left|right]; assumption.
Qed.