Coq_99_part_1.coq

Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.
Proof.
 intros.
 apply H.
 apply H1.
 apply H0.
 apply H1.
Qed.

Lemma Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
Proof.
 intros.
 destruct H.
 destruct H0.
 split.
 split.
 auto.
 auto.
 auto.
Qed.

Lemma Coq_03 : forall A B C D:Prop, (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D.
Proof.
 intros.
 destruct H.
 destruct H0.
 destruct H1.
 split.
 auto.
 auto.
Qed.

Lemma Coq_04 : forall A : Prop, ~(A /\ ~A).
Proof.
 unfold not.
 intros.
 destruct H.
 apply H0.
 apply H.
Qed.

Lemma Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C.
Proof.
 intros.
 destruct H.
 left.
 left.
 exact H.
 destruct H.
 left.
 right.
 exact H.
 right.
 exact H.
Qed.

Lemma Coq_06 : forall A, ~~~A -> ~A.
Proof.
 intros.
 unfold not.
 unfold not in H.
 intros.
 apply H.
 intros.
 apply H1.
 exact H0.
Qed.

Lemma Coq_07 : forall A B:Prop, (A->B)->~B->~A.
Proof.
 unfold not.
 intros.
 apply H0.
 apply H.
 apply H1.
Qed.

Lemma Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B.
Proof.
 intros.
 apply H.
 intros.
 apply H0.
 intros.
 apply H.
 intros.
 exact H1.
Qed.

Lemma Coq_09 : forall A:Prop, ~~(A\/~A).
Proof.
 unfold not.
 intros.
 apply H.
 right.
 intros.
 apply H.
 left.
 exact H0.
Qed.