Section Propositionnel.
Variables P Q R : Prop.

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

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

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

Theorem circuit :  (P <-> (~ P)) -> False.
Proof.
(* compléter *)  
Qed.

End Propositionnel.

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

Theorem notexists : (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).
Proof.
(* compléter *)  
Qed.

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.

Section Relations.

  Variable A : Set.

  Definition RTot (R : A -> A -> Prop) := forall x, exists y, R x y.

  (* TODO Définir RFun, Inj et Surj *)

  Definition Inv (R : A -> A -> Prop) x y := R y x.

  Theorem inj_fun_inv : forall R, Inj R -> RFun (Inv R).
  Proof.
    (* compléter *)
  Qed.

  Theorem fun_inj_inv : forall R, RFun R -> Inj (Inv R).
  Proof.
    (* compléter *)
  Qed.

  Theorem tot_surj_inv : forall R, RTot R -> Surj (Inv R).
  Proof.
    (* compléter *)
  Qed.

End Relations.

Section Fonctions.

  Variable A : Set.

  Definition FInj (f : A -> A) := forall x y, f x = f y -> x = y.

  Definition FSurj (f : A -> A) := (* compléter *).

  Definition Comp (f : A -> A) (g : A -> A) x := (* compléter *).

  Theorem comp_inj : forall f g, FInj f -> FInj g -> FInj (Comp f g).
  Proof.
    (* compléter *)
  Qed.

  Theorem comp_surj : forall f g, FSurj f -> FSurj g -> FSurj (Comp f g).
  Proof.
    (* compléter *)
  Qed.

End Fonctions.