Theorem un :
 forall P Q R : Prop, (P /\ Q) -> R -> (Q /\ R).
Proof.
(* compléter *)  
Qed.
  
Theorem uncurry : forall P Q R : Prop, (P -> Q -> R) -> (P /\ Q -> R).
Proof.
(* compléter *)  
Qed.

Theorem contra : forall P Q : Prop, (P -> Q) -> ~Q -> ~P.
Proof.
(* compléter *)  
Qed.

Theorem quatre : forall P Q R : Prop, (P \/ (Q /\ R)) -> P \/ Q.
Proof.
(* compléter *)  
Qed.


Section Quantificateurs.
Variable p : nat -> Prop.
Theorem fimpe : (forall x:nat, p x) -> exists y:nat, p y.
Proof.
(* compléter *)  
Qed.

Variable rel : nat -> nat -> Prop.
Theorem effe : (exists x, forall y, rel x y) -> (forall y, exists x, rel x y).
Proof.
(* compléter *)  
Qed.

Definition le (x y:nat) : Prop := exists z:nat, y = x + z.

Theorem plus_croissante : forall x y:nat, le x (x+y).

Require Import Omega.

Theorem le_refl : forall x:nat, le x x.
Proof.
(* compléter *)  
Qed.

Theorem le_trans : forall (x y z:nat), le x y /\ le y z -> le x z.
Proof.
(* compléter *)  
Qed.

End Quantificateurs.

Section PurPire.
  
Variable habitant : Set.
Variable pur : habitant -> Prop.
Variable pire : habitant -> Prop.
Axiom pur_ou_pire : forall x, pur x \/ pire x.

Variable say : habitant -> Prop -> Prop.
Axiom ax_pur : forall x P, pur x -> say x P -> P.
Axiom ax_pire : forall x P, pire x -> say x P -> ~P.


End PurPire.