Require Import Max.
Require Export tools.

Lemma first_N : forall N : nat, N >= 2 -> first N < N.
intros; unfold first in |- *; case (N_classic N); intro.
absurd (N >= 2).
elim s; intro y; rewrite y; unfold ge in |- *; auto with arith real.
exact H.
case (exist_first N g); intros; elim a; intros; elim H1; intros;
 auto with arith real.
Qed.

Lemma last_N : forall N : nat, N >= 2 -> last N < N.
intros; unfold last in |- *; case (N_classic N); intro.
absurd (N >= 2).
elim s; intro y; rewrite y; unfold ge in |- *; auto with arith real.
exact H.
case (exist_last N g); intros; elim a; intros; elim H1; intros;
 auto with arith real.
Qed.

Lemma inter1 : forall N : nat, N >= 2 -> max (first N) (last N) < N.
intros; apply max_case2.
apply (first_N N H).
apply (last_N N H).
Qed.

Lemma first_N01 : forall N : nat, first N <= N.
intros; unfold first in |- *; case (N_classic N); intro; auto with arith real.
case (exist_first N g); intros; elim a; intros; elim H0; intros;
 auto with arith real.
Qed.

Lemma last_N01 : forall N : nat, last N <= N.
intros; unfold last in |- *; case (N_classic N); intro; auto with arith real.
case (exist_last N g); intros; elim a; intros; elim H0; intros;
 auto with arith real.
Qed.

Lemma first_0 : forall N : nat, N >= 2 -> 0 < first N.
intros; unfold first in |- *; case (N_classic N); intro.
absurd (N >= 2).
elim s; intro y; rewrite y; unfold ge in |- *; auto with arith real.
exact H.
case (exist_first N g); intros; elim a; intros; auto with arith real.
Qed.

Lemma last_0 : forall N : nat, N >= 2 -> 0 < last N.
intros; unfold last in |- *; case (N_classic N); intro.
absurd (N >= 2).
elim s; intro y; rewrite y; unfold ge in |- *; auto with arith real.
exact H.
case (exist_last N g); intros; elim a; intros; auto with arith real.
Qed.

Lemma first_n :
 forall N n : nat,
 N >= 2 ->
 0 < n ->
 n < N ->
 (0 < alpha)%R /\ (alpha < 1)%R ->
 (frac_part_n_alpha (first N) <= frac_part_n_alpha n)%R.
intros; unfold first in |- *; case (N_classic N); intro.
absurd (N >= 2).
elim s; intro y; rewrite y; unfold ge in |- *; auto with arith real.
exact H.
case (exist_first N g); unfold ordre_total in |- *; intros; elim a; intros.
elim H4; intros.
generalize (H6 n); intros.
elim H7.
intro; apply Rlt_le; auto with arith real.
unfold Rle in |- *; auto with arith real.
split; auto with arith real.
auto with arith real.
Qed.

Lemma last_n :
 forall N n : nat,
 N >= 2 ->
 0 < n ->
 n < N ->
 (0 < alpha)%R /\ (alpha < 1)%R ->
 (frac_part_n_alpha n <= frac_part_n_alpha (last N))%R.
intros; unfold last in |- *; case (N_classic N); intro.
absurd (N >= 2).
elim s; intro y; rewrite y; unfold ge in |- *; auto with arith real.
exact H.
case (exist_last N g); unfold ordre_total in |- *; intros; elim a; intros.
elim H4; intros.
generalize (H6 n); intros.
elim H7.
intro; apply Rlt_le; auto with arith real.
unfold Rle in |- *; auto with arith real.
split; auto with arith real.
auto with arith real.
Qed.

Lemma tech_first_last :
 forall N k : nat,
 N >= 2 ->
 0 < k -> k < N -> ordre_total (first N) k /\ ordre_total k (last N).
intros; split; unfold ordre_total in |- *; intro.
apply (first_n N k H H0 H1 H2).
apply (last_n N k H H0 H1 H2).
Qed.

Lemma le_first_last :
 forall N : nat, N >= 2 -> ordre_total (first N) (last N).
intros; unfold ordre_total in |- *; intro.
apply (first_n N (last N) H (last_0 N H) (last_N N H) H0).
Qed.