# Library ThreeGap.prop_fl

Require Export prop_elem.
Require Export Classical_Prop.

Section theoreme.
Hypothesis alpha_irr : forall n p : Z, (alpha * IZR p)%R <> IZR n.
Hypothesis prop_alpha : (0 < alpha)%R /\ (alpha < 1)%R.
Hypothesis prop_N : forall N : nat, N >= 2.

Lemma tech_fp_alp_irr :
forall n m : nat, frac_part_n_alpha n = frac_part_n_alpha m -> n = m.
intros;
generalize (Rminus_diag_eq (frac_part_n_alpha n) (frac_part_n_alpha m) H);
unfold frac_part_n_alpha in |- *;
elim (Rminus_fp1 (INR n * alpha) (INR m * alpha)).
unfold Rminus in |- *; rewrite <- Ropp_mult_distr_l_reverse;
rewrite (Rmult_comm (INR n) alpha); rewrite (Rmult_comm (- INR m) alpha);
rewrite <- Rmult_plus_distr_l; intro;
elim (fp_nat (alpha * (INR n + - INR m)) H0); intros;
fold (INR n - INR m)%R in H1; rewrite (INR_IZR_INZ n) in H1;
rewrite (INR_IZR_INZ m) in H1;
rewrite (Z_R_minus (Z_of_nat n) (Z_of_nat m)) in H1;
generalize (alpha_irr x (Z_of_nat n - Z_of_nat m));
intro; elimtype False; auto.
unfold Rge in |- *; auto.
Qed.

Lemma fp_first_R0 : forall N : nat, (frac_part_n_alpha (first N) > 0)%R.
intro; generalize (P1 (first N)); intro; unfold Rle in H; unfold Rgt in |- *;
elim H; intro; auto; clear H; rewrite <- fp_R0 in H0;
rewrite <- (Rmult_0_l alpha) in H0; cut (INR 0 = 0%R).
intro; rewrite <- H in H0;
cut (frac_part (INR 0 * alpha) = frac_part_n_alpha 0).
intro; rewrite H1 in H0; generalize (tech_fp_alp_irr 0 (first N) H0); intro;
generalize (first_0 N (prop_N N)); intro;
generalize (lt_not_eq 0 (first N) H3); intro; elimtype False;
auto.
unfold frac_part_n_alpha in |- *; auto.
auto.
Qed.

Lemma contra_tech_fp_alp_irr :
forall n m : nat, n <> m -> frac_part_n_alpha n <> frac_part_n_alpha m.
intros; generalize (tech_fp_alp_irr n m); tauto.
Qed.

forall N k : nat,
N <= k ->
k < first N + last N ->
(frac_part_n_alpha k < frac_part_n_alpha (first N))%R \/
(frac_part_n_alpha k > frac_part_n_alpha (last N))%R -> False.
intros; elim H1; intro; clear H1.
cut
((frac_part_n_alpha (last N) -
(frac_part_n_alpha k - frac_part_n_alpha (first N) + 1))%R = 0%R).
unfold frac_part_n_alpha in |- *;
rewrite <- (Rminus_fp2 (INR k * alpha) (INR (first N) * alpha) H2);
generalize
(Rminus_fp1 (INR (last N) * alpha) (INR k * alpha - INR (first N) * alpha));
intros;
cut
(frac_part (INR (last N) * alpha) >=
frac_part (INR k * alpha - INR (first N) * alpha))%R.
intro; rewrite <- (H1 H4) in H3; clear H1 H4;
elim
(fp_nat (INR (last N) * alpha - (INR k * alpha - INR (first N) * alpha)) H3).
unfold Rminus in |- *;
rewrite <- (Ropp_mult_distr_l_reverse (INR (first N)) alpha);
rewrite (Ropp_plus_distr (INR k * alpha) (- INR (first N) * alpha));
rewrite <- (Ropp_mult_distr_l_reverse (INR k) alpha);
rewrite <- (Ropp_mult_distr_l_reverse (- INR (first N)) alpha);
rewrite (Ropp_involutive (INR (first N)));
rewrite (Rmult_comm (- INR k) alpha);
rewrite (Rmult_comm (INR (first N)) alpha);
rewrite (Rmult_comm (INR (last N)) alpha);
rewrite <- (Rmult_plus_distr_l alpha (- INR k) (INR (first N)));
rewrite <-
(Rmult_plus_distr_l alpha (INR (last N)) (- INR k + INR (first N)))
; rewrite (Rplus_comm (- INR k) (INR (first N)));
rewrite <- (Rplus_assoc (INR (last N)) (INR (first N)) (- INR k));
fold (INR (last N) + INR (first N) - INR k)%R in |- *;
rewrite <- (plus_INR (last N) (first N));
rewrite (INR_IZR_INZ (last N + first N)).
rewrite (INR_IZR_INZ k).
rewrite (Z_R_minus (Z_of_nat (last N + first N)) (Z_of_nat k)).
intros.
generalize (alpha_irr x (Z_of_nat (last N + first N) - Z_of_nat k)).
intro.
auto.
unfold Rge in |- *; right; apply Rminus_diag_uniq; auto.
cut
((frac_part_n_alpha k - frac_part_n_alpha (first N) + 1 <=
frac_part_n_alpha (last N))%R /\
(frac_part_n_alpha k - frac_part_n_alpha (last N) + 1 >=
frac_part_n_alpha (first N))%R).
intro; elim H1; intros; clear H1.
generalize
(Rle_minus (frac_part_n_alpha k - frac_part_n_alpha (first N) + 1)
(frac_part_n_alpha (last N)) H3);
generalize
(Rge_minus (frac_part_n_alpha k - frac_part_n_alpha (last N) + 1)
(frac_part_n_alpha (first N)) H4); intros; clear H3 H4;
generalize
(Rge_le
(frac_part_n_alpha k - frac_part_n_alpha (last N) + 1 -
frac_part_n_alpha (first N)) 0 H1); intro; clear H1;
rewrite <- Ropp_minus_distr; rewrite <- Ropp_0; apply Ropp_eq_compat.
unfold Rminus in H3;
rewrite (Rplus_comm (frac_part_n_alpha k) (- frac_part_n_alpha (last N)))
in H3;
rewrite (Rplus_assoc (- frac_part_n_alpha (last N)) (frac_part_n_alpha k) 1)
in H3.
rewrite
(Rplus_assoc (- frac_part_n_alpha (last N)) (frac_part_n_alpha k + 1)
(- frac_part_n_alpha (first N))) in H3;
rewrite
(Rplus_comm (- frac_part_n_alpha (last N))
(frac_part_n_alpha k + 1 + - frac_part_n_alpha (first N)))
in H3;
rewrite
(Rplus_assoc (frac_part_n_alpha k) 1 (- frac_part_n_alpha (first N)))
in H3; rewrite (Rplus_comm 1 (- frac_part_n_alpha (first N))) in H3;
rewrite <-
(Rplus_assoc (frac_part_n_alpha k) (- frac_part_n_alpha (first N)) 1)
in H3; fold (frac_part_n_alpha k - frac_part_n_alpha (first N))%R in H3;
fold
(frac_part_n_alpha k - frac_part_n_alpha (first N) + 1 -
frac_part_n_alpha (last N))%R in H3;
elim
(Rle_le_eq
(frac_part_n_alpha k - frac_part_n_alpha (first N) + 1 -
frac_part_n_alpha (last N)) 0); auto.
split; unfold frac_part_n_alpha in |- *.
unfold frac_part_n_alpha in H2;
rewrite <- (Rminus_fp2 (INR k * alpha) (INR (first N) * alpha) H2);
elim (tech_first_last N (k - first N) (prop_N N)).
intros; unfold ordre_total in H3; unfold frac_part_n_alpha in H3;
cut (first N <= k).
intro; rewrite (minus_INR k (first N) H4) in H3; unfold Rminus in H3;
rewrite (Rmult_comm (INR k + - INR (first N)) alpha) in H3;
rewrite (Rmult_plus_distr_l alpha (INR k) (- INR (first N))) in H3;
rewrite (Rmult_comm alpha (- INR (first N))) in H3;
rewrite (Ropp_mult_distr_l_reverse (INR (first N)) alpha) in H3;
fold (alpha * INR k - INR (first N) * alpha)%R in H3;
rewrite (Rmult_comm alpha (INR k)) in H3; auto.
generalize (first_N01 N); intro; apply (le_trans (first N) N k H4 H).
elim (lt_minus2 (first N) k); auto.
generalize (first_N N (prop_N N)); intro.
apply (lt_le_trans (first N) N k H1 H).
cut (k - first N < last N).
generalize (last_N01 N); intros;
apply (lt_le_trans (k - first N) (last N) N H3 H1).
apply (lt_plus_minus k (first N) (last N)).
generalize (first_N N (prop_N N)); intro;
apply (lt_le_trans (first N) N k H1 H).
assumption.
cut (frac_part_n_alpha k < frac_part_n_alpha (last N))%R.
intro; unfold frac_part_n_alpha in H1;
rewrite <- (Rminus_fp2 (INR k * alpha) (INR (last N) * alpha) H1);
elim (tech_first_last N (k - last N) (prop_N N)).
intros; unfold ordre_total in H3; unfold frac_part_n_alpha in H3;
cut (last N <= k).
intro; rewrite (minus_INR k (last N) H5) in H3; unfold Rminus in H3;
rewrite (Rmult_comm (INR k + - INR (last N)) alpha) in H3;
rewrite (Rmult_plus_distr_l alpha (INR k) (- INR (last N))) in H3;
rewrite (Rmult_comm alpha (- INR (last N))) in H3;
rewrite (Ropp_mult_distr_l_reverse (INR (last N)) alpha) in H3;
fold (alpha * INR k - INR (last N) * alpha)%R in H3;
rewrite (Rmult_comm alpha (INR k)) in H3;
apply
(Rle_ge (frac_part (INR (first N) * alpha))
(frac_part (INR k * alpha - INR (last N) * alpha))
(H3 prop_alpha)).
generalize (last_N01 N); intro; apply (le_trans (last N) N k H5 H).
elim (lt_minus2 (last N) k); auto.
generalize (last_N N (prop_N N)); intro.
apply (lt_le_trans (last N) N k H3 H).
cut (k - last N < first N).
generalize (first_N01 N); intros;
apply (lt_le_trans (k - last N) (first N) N H4 H3).
apply (lt_plus_minus k (last N) (first N)).
generalize (last_N N (prop_N N)); intro;
apply (lt_le_trans (last N) N k H3 H).
rewrite plus_comm; assumption.
generalize (le_first_last N (prop_N N)); unfold ordre_total in |- *; intros;
apply
(Rlt_le_trans (frac_part_n_alpha k) (frac_part_n_alpha (first N))
(frac_part_n_alpha (last N)) H2 (H1 prop_alpha)).
cut
((frac_part_n_alpha (last N) -
(frac_part_n_alpha k - frac_part_n_alpha (first N)))%R = 0%R).
cut (frac_part_n_alpha k >= frac_part_n_alpha (first N))%R.
unfold frac_part_n_alpha in |- *; intro;
rewrite <- (Rminus_fp1 (INR k * alpha) (INR (first N) * alpha) H1);
generalize
(Rminus_fp1 (INR (last N) * alpha) (INR k * alpha - INR (first N) * alpha));
intros;
cut
(frac_part (INR (last N) * alpha) >=
frac_part (INR k * alpha - INR (first N) * alpha))%R.
intro; rewrite <- (H3 H5) in H4; clear H3 H5;
elim
(fp_nat (INR (last N) * alpha - (INR k * alpha - INR (first N) * alpha)) H4).
unfold Rminus in |- *;
rewrite <- (Ropp_mult_distr_l_reverse (INR (first N)) alpha);
rewrite (Ropp_plus_distr (INR k * alpha) (- INR (first N) * alpha));
rewrite <- (Ropp_mult_distr_l_reverse (INR k) alpha);
rewrite <- (Ropp_mult_distr_l_reverse (- INR (first N)) alpha);
rewrite (Ropp_involutive (INR (first N)));
rewrite (Rmult_comm (- INR k) alpha);
rewrite (Rmult_comm (INR (first N)) alpha);
rewrite (Rmult_comm (INR (last N)) alpha);
rewrite <- (Rmult_plus_distr_l alpha (- INR k) (INR (first N)));
rewrite <-
(Rmult_plus_distr_l alpha (INR (last N)) (- INR k + INR (first N)))
; rewrite (Rplus_comm (- INR k) (INR (first N)));
rewrite <- (Rplus_assoc (INR (last N)) (INR (first N)) (- INR k));
fold (INR (last N) + INR (first N) - INR k)%R in |- *;
rewrite <- (plus_INR (last N) (first N)).
rewrite (INR_IZR_INZ (last N + first N)).
rewrite (INR_IZR_INZ k).
rewrite (Z_R_minus (Z_of_nat (last N + first N)) (Z_of_nat k)).
intros.
generalize (alpha_irr x (Z_of_nat (last N + first N) - Z_of_nat k)).
intro.
auto.
unfold Rge in |- *; right; apply Rminus_diag_uniq; auto.
generalize (le_first_last N (prop_N N)); unfold ordre_total in |- *; intros;
unfold Rgt in H2; cut (frac_part_n_alpha (first N) <= frac_part_n_alpha k)%R.
intro; apply (Rle_ge (frac_part_n_alpha (first N)) (frac_part_n_alpha k) H3).
cut (frac_part_n_alpha (first N) < frac_part_n_alpha k)%R.
intro; apply (Rlt_le (frac_part_n_alpha (first N)) (frac_part_n_alpha k) H3).
apply
(Rle_lt_trans (frac_part_n_alpha (first N)) (frac_part_n_alpha (last N))
(frac_part_n_alpha k) (H1 prop_alpha) H2).
cut
((frac_part_n_alpha k - frac_part_n_alpha (first N) <=
frac_part_n_alpha (last N))%R /\
(frac_part_n_alpha k - frac_part_n_alpha (last N) >=
frac_part_n_alpha (first N))%R).
intro; elim H1; intros; clear H1.
generalize
(Rle_minus (frac_part_n_alpha k - frac_part_n_alpha (first N))
(frac_part_n_alpha (last N)) H3);
generalize
(Rge_minus (frac_part_n_alpha k - frac_part_n_alpha (last N))
(frac_part_n_alpha (first N)) H4); intros; clear H3 H4;
generalize
(Rge_le
(frac_part_n_alpha k - frac_part_n_alpha (last N) -
frac_part_n_alpha (first N)) 0 H1); intro; clear H1;
rewrite <- Ropp_minus_distr; rewrite <- Ropp_0; apply Ropp_eq_compat.
unfold Rminus in H3;
rewrite
(Rplus_assoc (frac_part_n_alpha k) (- frac_part_n_alpha (last N))
(- frac_part_n_alpha (first N))) in H3;
rewrite
(Rplus_comm (- frac_part_n_alpha (last N)) (- frac_part_n_alpha (first N)))
in H3;
rewrite <-
(Rplus_assoc (frac_part_n_alpha k) (- frac_part_n_alpha (first N))
(- frac_part_n_alpha (last N))) in H3;
fold (frac_part_n_alpha k - frac_part_n_alpha (first N))%R in H3;
fold
(frac_part_n_alpha k - frac_part_n_alpha (first N) -
frac_part_n_alpha (last N))%R in H3;
elim
(Rle_le_eq
(frac_part_n_alpha k - frac_part_n_alpha (first N) -
frac_part_n_alpha (last N)) 0); auto.
split.
cut (frac_part_n_alpha k >= frac_part_n_alpha (first N))%R.
unfold frac_part_n_alpha in |- *; intro;
rewrite <- (Rminus_fp1 (INR k * alpha) (INR (first N) * alpha) H1);
elim (tech_first_last N (k - first N) (prop_N N)).
intros; unfold ordre_total in H4; unfold frac_part_n_alpha in H4;
cut (first N <= k).
intro; rewrite (minus_INR k (first N) H5) in H4; unfold Rminus in H4;
rewrite (Rmult_comm (INR k + - INR (first N)) alpha) in H4;
rewrite (Rmult_plus_distr_l alpha (INR k) (- INR (first N))) in H4;
rewrite (Rmult_comm alpha (- INR (first N))) in H4;
rewrite (Ropp_mult_distr_l_reverse (INR (first N)) alpha) in H4;
fold (alpha * INR k - INR (first N) * alpha)%R in H4;
rewrite (Rmult_comm alpha (INR k)) in H4; auto.
generalize (first_N01 N); intro; apply (le_trans (first N) N k H5 H).
elim (lt_minus2 (first N) k); auto.
generalize (first_N N (prop_N N)); intro.
apply (lt_le_trans (first N) N k H3 H).
cut (k - first N < last N).
generalize (last_N01 N); intros;
apply (lt_le_trans (k - first N) (last N) N H4 H3).
apply (lt_plus_minus k (first N) (last N)).
generalize (first_N N (prop_N N)); intro;
apply (lt_le_trans (first N) N k H3 H).
assumption.
unfold frac_part_n_alpha in |- *; generalize (le_first_last N (prop_N N));
unfold ordre_total in |- *; intros; unfold Rgt in H2;
cut (frac_part_n_alpha (first N) <= frac_part_n_alpha k)%R.
intro; apply (Rle_ge (frac_part_n_alpha (first N)) (frac_part_n_alpha k) H3).
cut (frac_part_n_alpha (first N) < frac_part_n_alpha k)%R.
intro; apply (Rlt_le (frac_part_n_alpha (first N)) (frac_part_n_alpha k) H3).
apply
(Rle_lt_trans (frac_part_n_alpha (first N)) (frac_part_n_alpha (last N))
(frac_part_n_alpha k) (H1 prop_alpha) H2).
cut (frac_part_n_alpha k >= frac_part_n_alpha (last N))%R.
unfold frac_part_n_alpha in |- *; intro;
rewrite <- (Rminus_fp1 (INR k * alpha) (INR (last N) * alpha) H1);
elim (tech_first_last N (k - last N) (prop_N N)).
intros; unfold ordre_total in H3; unfold frac_part_n_alpha in H3;
cut (last N <= k).
intro; rewrite (minus_INR k (last N) H5) in H3; unfold Rminus in H3;
rewrite (Rmult_comm (INR k + - INR (last N)) alpha) in H3;
rewrite (Rmult_plus_distr_l alpha (INR k) (- INR (last N))) in H3;
rewrite (Rmult_comm alpha (- INR (last N))) in H3;
rewrite (Ropp_mult_distr_l_reverse (INR (last N)) alpha) in H3;
fold (alpha * INR k - INR (last N) * alpha)%R in H3;
rewrite (Rmult_comm alpha (INR k)) in H3;
apply
(Rle_ge (frac_part (INR (first N) * alpha))
(frac_part (INR k * alpha - INR (last N) * alpha))
(H3 prop_alpha)).
generalize (last_N01 N); intro; apply (le_trans (last N) N k H5 H).
elim (lt_minus2 (last N) k); auto.
generalize (last_N N (prop_N N)); intro.
apply (lt_le_trans (last N) N k H3 H).
cut (k - last N < first N).
generalize (first_N01 N); intros;
apply (lt_le_trans (k - last N) (first N) N H4 H3).
apply (lt_plus_minus k (last N) (first N)).
generalize (last_N N (prop_N N)); intro;
apply (lt_le_trans (last N) N k H3 H).
rewrite plus_comm; assumption.
apply Rgt_ge; auto.
Qed.

Lemma absurd1 :
forall N k : nat,
N <= k ->
k < first N + last N ->
(frac_part_n_alpha k >= frac_part_n_alpha (first N))%R /\
(frac_part_n_alpha k <= frac_part_n_alpha (last N))%R.
intros; generalize (contradiction1 N k H H0); intro;
cut
(~ (frac_part_n_alpha k < frac_part_n_alpha (first N))%R /\
~ (frac_part_n_alpha k > frac_part_n_alpha (last N))%R).
intro; elim H2; intros; split.
apply (Rnot_lt_ge (frac_part_n_alpha k) (frac_part_n_alpha (first N)) H3).
apply (Rnot_gt_le (frac_part_n_alpha k) (frac_part_n_alpha (last N)) H4).
apply
(not_or_and (frac_part_n_alpha k < frac_part_n_alpha (first N))%R
(frac_part_n_alpha k > frac_part_n_alpha (last N))%R H1).
Qed.

Lemma absurd_first :
forall N k : nat,
0 < k ->
k < first N + last N ->
(frac_part_n_alpha (first N) <= frac_part_n_alpha k)%R.
intros; elim inser_trans_lt with 0 k (first N + last N) N.
intro y; elim y; intros; apply (first_n N k (prop_N N) H1 H2 prop_alpha).
intro y; elim y; intros.
elim (absurd1 N k H1 H2); intros.
unfold Rge in H3; unfold Rle in |- *; unfold Rgt in H3; elim H3; intro.
left; assumption.
right; auto.
auto.
Qed.

Lemma absurd_last :
forall N k : nat,
0 < k ->
k < first N + last N ->
(frac_part_n_alpha k <= frac_part_n_alpha (last N))%R.
intros; elim inser_trans_lt with 0 k (first N + last N) N.
intro y; elim y; intros; apply (last_n N k (prop_N N) H1 H2 prop_alpha).
intro y; elim y; intros.
elim (absurd1 N k H1 H2); intros; auto.
auto.
Qed.

Lemma tech_first_aux :
forall N a : nat,
0 < a ->
a < N ->
((forall b : nat,
0 < b -> b < N -> (frac_part_n_alpha a <= frac_part_n_alpha b)%R) <->
a = first N).
intros; split; intro.
cut (frac_part_n_alpha a = frac_part_n_alpha (first N)).
intro; apply (tech_fp_alp_irr a (first N) H2).
elim (Rle_le_eq (frac_part_n_alpha a) (frac_part_n_alpha (first N))); intros;
clear H3;
generalize (H1 (first N) (first_0 N (prop_N N)) (first_N N (prop_N N)));
generalize (first_n N a (prop_N N) H H0 prop_alpha);
intros; apply H2.
split; auto.
intros; rewrite H1; apply (first_n N b (prop_N N) H2 H3 prop_alpha).
Qed.

Lemma eq_first_M_N :
forall N M : nat,
M = first N + last N ->
((forall b : nat,
0 < b -> b < M -> (frac_part_n_alpha (first N) <= frac_part_n_alpha b)%R) <->
first N = first M).
intros; split; intro.
elim (tech_first_aux M (first N) (first_0 N (prop_N N))).
intros; clear H2; auto.
rewrite H; apply (lt_plus (first N) (last N) (last_0 N (prop_N N))).
elim
(tech_first_aux M (first M) (first_0 M (prop_N M)) (first_N M (prop_N M))).
intros; clear H1; rewrite H0; auto.
Qed.

Lemma first_eq_M_N :
forall N M : nat, M = first N + last N -> first N = first M.
intros; elim (eq_first_M_N N M H); intros; clear H1; apply H0.
intros; rewrite H in H2; apply (absurd_first N b H1 H2).
Qed.

Lemma tech_last_aux :
forall N a : nat,
0 < a ->
a < N ->
((forall b : nat,
0 < b -> b < N -> (frac_part_n_alpha b <= frac_part_n_alpha a)%R) <->
a = last N).
intros; split; intro.
cut (frac_part_n_alpha a = frac_part_n_alpha (last N)).
intro; apply (tech_fp_alp_irr a (last N) H2).
elim (Rle_le_eq (frac_part_n_alpha a) (frac_part_n_alpha (last N))); intros;
clear H3;
generalize (H1 (last N) (last_0 N (prop_N N)) (last_N N (prop_N N)));
generalize (last_n N a (prop_N N) H H0 prop_alpha);
intros; apply H2.
split; auto.
intros; rewrite H1; apply (last_n N b (prop_N N) H2 H3 prop_alpha).
Qed.

Lemma eq_last_M_N :
forall N M : nat,
M = first N + last N ->
((forall b : nat,
0 < b -> b < M -> (frac_part_n_alpha b <= frac_part_n_alpha (last N))%R) <->
last N = last M).
intros; split; intro.
elim (tech_last_aux M (last N) (last_0 N (prop_N N))).
intros; clear H2; auto.
rewrite H; rewrite plus_comm;
apply (lt_plus (last N) (first N) (first_0 N (prop_N N))).
elim (tech_last_aux M (last M) (last_0 M (prop_N M)) (last_N M (prop_N M))).
intros; clear H1; rewrite H0; auto.
Qed.

Lemma last_eq_M_N : forall N M : nat, M = first N + last N -> last N = last M.
intros; elim (eq_last_M_N N M H); intros; clear H1; apply H0.
intros; rewrite H in H2; apply (absurd_last N b H1 H2).
Qed.

Lemma tech_after :
forall N n m : nat,
0 < n ->
n < N ->
0 <= m ->
m < N ->
(frac_part_n_alpha n < frac_part_n_alpha m)%R ->
((exists k : nat,
0 < k /\
k < N /\
(frac_part_n_alpha n < frac_part_n_alpha k)%R /\
(frac_part_n_alpha k < frac_part_n_alpha m)%R) -> False) ->
m = after N n.
intros; unfold after in |- *.
case (exist_after_M (frac_part_n_alpha n) (P1 n) (P2 n) N); intro.
elim s; intros x y.
elim y; intros.
clear s y.
elim H6; intros; clear H6.
elim H8; intros; clear H8.
generalize
(tech_not_exist_pt (fun k : nat => 0 < k) (fun k : nat => k < N)
(fun k : nat => (frac_part_n_alpha n < frac_part_n_alpha k)%R)
(fun k : nat => (frac_part_n_alpha k < frac_part_n_alpha m)%R) H4);
clear H4; intro.
elim (H4 x H5 H7); intro.
absurd (frac_part_n_alpha n < frac_part_n_alpha x)%R; auto.
unfold Rgt in H9; generalize (H9 m H1 H2 H3); intro;
generalize (Rnot_lt_ge (frac_part_n_alpha x) (frac_part_n_alpha m) H8);
intro;
generalize (Rge_antisym (frac_part_n_alpha m) (frac_part_n_alpha x) H10 H11);
intro; apply (tech_fp_alp_irr m x H12).
elim (a m H1 H2); intros; unfold Rle in H6; elim H6; intro.
generalize (Rlt_asym (frac_part_n_alpha m) (frac_part_n_alpha n) H7); intro;
elimtype False; auto.
cut
((frac_part_n_alpha n < frac_part_n_alpha m)%R \/
(frac_part_n_alpha n > frac_part_n_alpha m)%R).
intro;
generalize
(Rlt_dichotomy_converse (frac_part_n_alpha n) (frac_part_n_alpha m) H8);
intro; elimtype False; auto.
left; auto.
Qed.

Lemma prop_after :
forall N n m : nat,
after N n = m ->
(exists k : nat,
0 < k /\
k < N /\
(frac_part_n_alpha n < frac_part_n_alpha k)%R /\
(frac_part_n_alpha k < frac_part_n_alpha m)%R) -> False.
intros; elim H0; intros; elim H1; intros; elim H3; intros; elim H5; intro;
clear H0 H1 H3 H5; rewrite <- H; unfold after in |- *;
case (exist_after_M (frac_part_n_alpha n) (P1 n) (P2 n) N);
intro.
elim s; intros x0 y H0; elim y; intros; elim H3; intros; elim H7; intros;
clear s y H3 H7; fold (frac_part_n_alpha x > frac_part_n_alpha n)%R in H6;
generalize (H9 x (lt_le_weak 0 x H2) H4 H6); intro;
generalize (Rgt_not_le (frac_part_n_alpha x0) (frac_part_n_alpha x) H0);
intro; cut (frac_part_n_alpha x0 <= frac_part_n_alpha x)%R.
intro; auto.
unfold Rge in H3; unfold Rle in |- *; elim H3; auto.
unfold frac_part_n_alpha in |- *; simpl in |- *; rewrite (Rmult_0_l alpha);
rewrite fp_R0; elim (base_fp (INR x * alpha)); intros;
generalize (Rgt_not_le 0 (frac_part (INR x * alpha)) H3);
intro; cut (0 <= frac_part (INR x * alpha))%R.
intro; auto.
unfold Rge in H0; unfold Rle in |- *; elim H0; auto.
Qed.

Lemma tech_after_lt :
forall N n m : nat,
0 < n ->
n < N ->
m <> 0 -> after N n = m -> (frac_part_n_alpha n < frac_part_n_alpha m)%R.
intros; rewrite <- H2; unfold after in |- *;
case (exist_after_M (frac_part_n_alpha n) (P1 n) (P2 n) N);
intros.
elim s; intros x y.
elim y; intros; clear y.
elim H4; intros; clear H4.
elim H6; intros; clear H6; auto.
cut (after N n = 0).
intro; rewrite H2 in H3; elimtype False; auto.
unfold after in |- *;
case (exist_after_M (frac_part_n_alpha n) (P1 n) (P2 n) N);
intros; auto.
elim s; intros x y.
elim y; intros; clear y.
elim H4; intros; clear H4.
elim H6; intros; clear H6; clear s.
generalize (lt_le_weak 0 x H3); intro.
elim (a x H6 H5); intros.
unfold Rle in H9; elim H9; intro; clear H9.
generalize (Rlt_asym (frac_part_n_alpha n) (frac_part_n_alpha x) H4); intro;
elimtype False; auto.
generalize (sym_eq H10); intro; clear H10.
cut
((frac_part_n_alpha n < frac_part_n_alpha x)%R \/
(frac_part_n_alpha n > frac_part_n_alpha x)%R); auto.
intro;
generalize
(Rlt_dichotomy_converse (frac_part_n_alpha n) (frac_part_n_alpha x) H10);
intro; elimtype False; auto.
Qed.

Lemma after_last : forall N : nat, after N (last N) = 0.
unfold after in |- *; intro;
case
(exist_after_M (frac_part_n_alpha (last N)) (P1 (last N)) (P2 (last N)) N);
auto.
intro; elim s; intros x y; elim y; intros; elim H0; intros; elim H2; intros;
clear s y H0 H2 H4; generalize (last_n N x (prop_N N) H H1 prop_alpha);
intro;
generalize
(Rgt_not_le (frac_part_n_alpha x) (frac_part_n_alpha (last N)) H3);
intro; elimtype False; auto.
Qed.

Lemma prop_M :
forall N M : nat,
M = first N + last N ->
(frac_part_n_alpha M < frac_part_n_alpha (first N))%R \/
(frac_part_n_alpha M > frac_part_n_alpha (last N))%R.
intros; rewrite H;
cut
((frac_part_n_alpha (first N) + frac_part_n_alpha (last N) < 1)%R \/
(frac_part_n_alpha (first N) + frac_part_n_alpha (last N) >= 1)%R).
intros; elim H0; intro; clear H0.
right; unfold frac_part_n_alpha in H1; unfold frac_part_n_alpha in |- *;
rewrite (plus_INR (first N) (last N));
rewrite (Rmult_comm (INR (first N) + INR (last N)) alpha);
rewrite (Rmult_plus_distr_l alpha (INR (first N)) (INR (last N)));
rewrite (Rmult_comm (INR (first N)) alpha) in H1;
rewrite (Rmult_comm (INR (last N)) alpha) in H1;
rewrite (Rmult_comm (INR (last N)) alpha);
rewrite (plus_frac_part2 (alpha * INR (first N)) (alpha * INR (last N)) H1);
elim (Rplus_ne (alpha * INR (last N))); intros; clear H0;
pattern (alpha * INR (last N))%R at 2 in |- *; rewrite <- H2;
rewrite
(Rplus_comm (frac_part (alpha * INR (first N)))
(frac_part (alpha * INR (last N))));
rewrite (Rplus_comm 0 (alpha * INR (last N)));
cut (frac_part (alpha * INR (last N)) + frac_part 0 < 1)%R.
intro; rewrite (plus_frac_part2 (alpha * INR (last N)) 0 H0); rewrite fp_R0;
apply
(Rplus_gt_compat_l (frac_part (alpha * INR (last N)))
(frac_part (alpha * INR (first N))) 0); generalize (fp_first_R0 N);
unfold frac_part_n_alpha in |- *; rewrite (Rmult_comm alpha (INR (first N)));
auto.
rewrite fp_R0; elim (Rplus_ne (frac_part (alpha * INR (last N)))); intros;
clear H3; rewrite H0; rewrite (Rmult_comm alpha (INR (last N)));
cut (frac_part (INR (last N) * alpha) = frac_part_n_alpha (last N)).
intro; rewrite H3; apply (P2 (last N)).
unfold frac_part_n_alpha in |- *; auto.
left; unfold frac_part_n_alpha in H1; unfold frac_part_n_alpha in |- *;
unfold frac_part_n_alpha in |- *; rewrite (plus_INR (first N) (last N));
rewrite (Rmult_comm (INR (first N) + INR (last N)) alpha);
rewrite (Rmult_plus_distr_l alpha (INR (first N)) (INR (last N)));
rewrite (Rmult_comm (INR (first N)) alpha) in H1;
rewrite (Rmult_comm (INR (last N)) alpha) in H1;
rewrite (Rmult_comm (INR (first N)) alpha);
rewrite (plus_frac_part1 (alpha * INR (first N)) (alpha * INR (last N)) H1);
unfold Rminus in |- *; rewrite Rplus_assoc;
elim (Rplus_ne (alpha * INR (first N))); intros; clear H2;
pattern (alpha * INR (first N))%R at 2 in |- *; rewrite <- H0;
cut (frac_part (alpha * INR (first N)) + frac_part 0 < 1)%R.
intro; rewrite (plus_frac_part2 (alpha * INR (first N)) 0 H2); rewrite fp_R0;
apply
(Rplus_lt_compat_l (frac_part (alpha * INR (first N)))
(frac_part (alpha * INR (last N)) + -1) 0);
cut
((frac_part (alpha * INR (last N)) + -1)%R =
(frac_part (alpha * INR (last N)) - 1)%R).
intro; rewrite H3; clear H3;
apply (Rlt_minus (frac_part (alpha * INR (last N))) 1).
rewrite (Rmult_comm alpha (INR (last N)));
cut (frac_part (INR (last N) * alpha) = frac_part_n_alpha (last N)).
intro; rewrite H3; apply (P2 (last N)).
unfold frac_part_n_alpha in |- *; auto.
unfold Rminus in |- *; auto.
rewrite fp_R0; elim (Rplus_ne (frac_part (alpha * INR (first N)))); intros;
clear H3; rewrite H2; rewrite (Rmult_comm alpha (INR (first N)));
cut (frac_part (INR (first N) * alpha) = frac_part_n_alpha (first N)).
intro; rewrite H3; apply (P2 (first N)).
unfold frac_part_n_alpha in |- *; auto.
unfold Rge in |- *;
generalize
(Rtotal_order (frac_part_n_alpha (first N) + frac_part_n_alpha (last N)) 1);
intro; elim H0; intro.
left; auto.
right; elim H1; auto.
Qed.

Lemma le_N_M : forall N M : nat, M = first N + last N -> N <= M.
intros; generalize (prop_M N M H); intro; cut (~ N > M).
intro; apply not_gt_le; auto.
unfold gt in |- *; red in |- *; intro; cut (0 < M).
intro; elim H0; intro; clear H0.
generalize (first_n N M (prop_N N) H2 H1 prop_alpha); intro.
generalize
(Rgt_not_le (frac_part_n_alpha (first N)) (frac_part_n_alpha M) H3);
intro; clear H3; auto.
generalize (last_n N M (prop_N N) H2 H1 prop_alpha); intro.
unfold Rgt in H3;
generalize
(Rgt_not_le (frac_part_n_alpha M) (frac_part_n_alpha (last N)) H3);
intro; clear H3; auto.
rewrite H; generalize (first_0 N (prop_N N)); intro;
apply (lt_O_plus (first N) (last N) H2).
Qed.

End theoreme.