Section Propositional_logic.

Section Basic_facts.

Variables P Q R T: Prop.

Lemma and_commutative: 
P /\ Q -> Q /\ P.
intro c.
elim c;intro p;intro q.
split.
assumption.
assumption.
Qed.
Print and_commutative.

Lemma and_associative:
(P /\ Q) /\ R -> P /\ (Q /\ R).
Proof.
intro H.
elim H. intro c. intro r.
elim c. intro p. intro q.
split.
assumption.
split. assumption. assumption.
Qed.
Print and_associative.
End Basic_facts.

Variables P Q R T: Prop.

Print and_commutative.
Lemma and_commutative_both:
P /\ Q <-> Q /\ P.
Proof.
split.
apply and_commutative.
apply and_commutative.
Qed.
Print and_commutative_both.


Lemma or_commutative: 
P \/ Q -> Q \/ P.
Proof.
intro d.
elim d.
intro p.
right. assumption.
intro q.
left. assumption.
Qed.
Print or_commutative.


Lemma or_distr:
P \/ (Q /\ R)  ->  (P\/Q)/\(P \/ R).
Proof.
intro H.
elim H.
intro p. 
split.
left. assumption.
left. assumption.
intro c.
elim c. intro q. intro r.
split.
right. assumption.
right. assumption.
Qed.
Print or_distr.