Theorem one_plus_one_is_two : 1 + 1 = 2.
Proof. trivial. Qed.
Theorem p_implies_p : forall P:Prop, P -> P.
Proof.
intros P. intros P_assumed. assumption.
Qed.
Theorem and_fst : forall P Q, P /\ Q -> P.
Proof.
intros P Q PandQ.
destruct PandQ as [P_holds Q_holds].
assumption.
Qed.
Theorem and_ex : 42=42 /\ 43=43.
Proof.
split. trivial. trivial.
Qed.
Theorem and_comm: forall P Q, P /\ Q -> Q /\ P.
Proof.
intros P Q PandQ.
destruct PandQ as [P_holds Q_holds].
split.
all: assumption.
Qed.
Theorem or_left : forall (P Q : Prop), P -> P \/ Q.
Proof.
intros P Q P_holds. left. assumption.
Qed.
Theorem or_comm : forall P Q, P \/ Q -> Q \/ P.
Proof.
intros P Q PorQ. destruct PorQ.
- right. assumption.
- left. assumption.
Qed.
Theorem explosion : forall P, False -> P.
Proof.
intros P false_holds. contradiction.
Qed.
Theorem contra_implies_anything : forall P Q, P /\ ~P -> Q.
Proof.
intros P Q PandnotP.
destruct PandnotP as [P_holds notP_holds].
contradiction.
Qed.