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.

Section ExoPair.

Inductive pair : nat -> Prop :=
| pair_0 : pair 0
| pair_s2 : forall x, pair x -> pair (S (S x)).

Check pair_ind.

Inductive impair : nat -> Prop := (* ... *)

Lemma spi : forall x, pair x -> impair (S x).
Proof.
(* ... *)
Qed.

Lemma sip : forall x, impair x -> pair (S x).
Proof.
(* ... *)
Qed.

Lemma poui : forall x, pair x \/ impair x.
Proof.
(* ... *)
Qed.

End ExoPair.