Section Propositional_Logic.
Variables P Q R T: Prop.

Theorem Konstante:
(P -> (Q -> P)).
Proof.
intro p.
intro q.
assumption.
Qed.
Print Konstante.

Theorem imp_trans: 
(P -> Q) -> (Q -> R) -> (P -> R).
intro f.
intro g.
intro p.
apply g.
apply f.
assumption.
Qed.
Print imp_trans.

Theorem imp_trans2: 
(P -> Q) -> (Q -> R) -> (P -> R).
auto.
Qed.
Print imp_trans2.

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

Theorem and_commutative: 
P /\ Q -> Q /\ P.
intro z.
elim z.
intro p.
intro q.
split.
assumption.
assumption.
Qed.
Print and_commutative.

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

End Propositional_Logic.