Inductive or3 (A B C : Prop) : Set :=
  | or3_Left : A → or3 A B C
  | or3_Middle : B → or3 A B C
  | or3_Right : C → or3 A B C.

Lemma sym_and : ∀ A B : Prop, A ∧ B → B ∧ A.
intros A B H; elim H; split; auto.
Qed.
Hint Immediate sym_and.

Lemma sym_or : ∀ A B : Prop, A ∨ B → B ∨ A.
simple induction 1; auto.
Qed.
Hint Immediate sym_or.

Lemma no_and_l : ∀ A B : Prop, ¬ A → ¬ (A ∧ B).
unfold not in |- ×.
intros A B H G; apply H.
elim G; auto.
Qed.
Hint Immediate no_and_l.

Lemma no_and_r : ∀ A B : Prop, ¬ B → ¬ (A ∧ B).
unfold not in |- ×.
intros A B H G; apply H.
elim G; auto.
Qed.
Hint Immediate no_and_r.

Lemma no_or : ∀ A B : Prop, ¬ A → B ∨ A → B.
intros A B H G; elim G; auto.
intro; absurd A; auto.
Qed.

Lemma no_or_inv : ∀ A B : Prop, ¬ A → A ∨ B → B.
intros A B H G; elim G; auto.
intro; absurd A; auto.
Qed.

Lemma no_or_and : ∀ A B C D : Prop, ¬ C → A ∧ B ∨ C ∧ D → A ∧ B.
intros.
apply no_or with (C ∧ D); auto.
Qed.

Lemma no_or_and_inv :
 ∀ A B C D : Prop, ¬ D → C ∧ D ∨ A ∧ B → A ∧ B.
intros.
apply no_or_inv with (C ∧ D); auto.
Qed.

Lemma no_no_A : ∀ A : Prop, A → ¬ ¬ A.
unfold not in |- *; auto.
Qed.
Hint Immediate no_no_A.

Lemma impl_no_no : ∀ A B : Prop, (A → B) → ¬ B → ¬ A.
unfold not in |- *; auto.
Qed.

Lemma no_or_r : ∀ A B : Prop, ¬ A → A ∨ B → B.
intros A B not_A A_or_B.
elim A_or_B; auto.
intro; absurd A; auto.
Qed.

Lemma no_or_l : ∀ A B : Prop, ¬ B → A ∨ B → A.
intros A B not_A A_or_B.
elim A_or_B; auto.
intro; absurd B; auto.
Qed.