Require Import Classical.

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.
    (* TODO *)
  Qed.

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

  Theorem tot_surj_inv : forall R, RTot R -> Surj (Inv R).
  Proof.
    (* TODO *)
  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) := (* TODO *)

  Definition Comp (f : A -> A) (g : A -> A) x := g (f x).

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

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

End Fonctions.

Section Ensembles_finis.

  Definition FFInj (n:nat) (f:nat->nat) :=
    forall x y, x<n -> y<n -> f(x)=f(y) -> x=y.

  Definition FFMono (n:nat) (f:nat->nat) :=
    forall x y, x<y -> y<n -> f(x)<f(y).

  Require Import Omega.

  Theorem mono_inj : forall f n, FFMono n f -> FFInj n f.
  Proof.
    (* TODO *)
  Qed.

  Theorem mono_domain :
     forall n f, FFMono (S n) f -> exists x, x<=n /\ f(x) >= n.
  Proof.
    (* TODO *)
  Qed.

End Ensembles_finis.