Require Import Classical_Prop.

Parameters A B C D : Prop.

(* Bei Unklarheiten können Sie das
   Coq-Intro auf der Webseite als
   Nachschlagewerk nutzen und auch
   Fragen im GLoIn-Forum stellen! *)

Lemma imp_transitive : (A -> B) -> (B -> C) -> (A -> C).
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.


Lemma negA : ~A -> (A -> False).
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.

Lemma proj3to1 : (A /\ B) -> (C -> A).
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.

Lemma curry : (A /\ B -> C) -> (A -> B -> C).
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.

Lemma eitherimp : (B \/ ~B) -> (A -> B) \/ (B -> C).
  (* Wie kann man es ohne Verwendung der Annahme
     (B \/ ~B) zeigen? *)
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.

Lemma contraposition : (~B -> ~A) -> (A -> B).
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.