Require Export prop_fl.

Section particular.
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.

Definition M (N : nat) := first N + last N.

Lemma inter31a :
 forall N n : nat, 0 < n -> n < last (M N) -> after (M N) n = n + first (M N).
intros; apply (sym_equal (x:=n + first (M N)) (y:=after (M N) n));
 apply (tech_after alpha_irr (M N) n (n + first (M N)) H);
 auto with arith real.
apply (lt_le_trans n (last (M N)) (M N) H0 (last_N01 (M N))).
unfold M at 2 in |- *;
 rewrite (last_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real;
 rewrite (first_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
rewrite (plus_comm (first (M N)) (last (M N)));
 apply (plus_lt_compat_r n (last (M N)) (first (M N)) H0).
fold (frac_part_n_alpha (n + first (M N)) > frac_part_n_alpha n)%R in |- *;
 apply
  (Rnot_le_lt (frac_part_n_alpha (n + first (M N))) (frac_part_n_alpha n));
 red in |- *; intro;
 generalize
  (Rplus_le_compat_l (- frac_part_n_alpha (first (M N)))
     (frac_part_n_alpha (n + first (M N))) (frac_part_n_alpha n) H1);
 rewrite
  (Rplus_comm (- frac_part_n_alpha (first (M N)))
     (frac_part_n_alpha (n + first (M N))));
 rewrite
  (Rplus_comm (- frac_part_n_alpha (first (M N))) (frac_part_n_alpha n))
  ;
 fold
  (frac_part_n_alpha (n + first (M N)) - frac_part_n_alpha (first (M N)))%R
  in |- *;
 fold (frac_part_n_alpha n - frac_part_n_alpha (first (M N)))%R in |- *;
 cut
  (frac_part_n_alpha (n + first (M N)) >= frac_part_n_alpha (first (M N)))%R.
intro; unfold frac_part_n_alpha at 1 2 in |- *;
 unfold frac_part_n_alpha in H2;
 rewrite <-
  (Rminus_fp1 (INR (n + first (M N)) * alpha) (INR (first (M N)) * alpha) H2)
  ; rewrite (plus_INR n (first (M N)));
 rewrite (Rmult_comm (INR n + INR (first (M N))) alpha);
 rewrite (Rmult_plus_distr_l alpha (INR n) (INR (first (M N))));
 rewrite (Rmult_comm alpha (INR (first (M N)))); unfold Rminus at 1 in |- *;
 rewrite
  (Rplus_assoc (alpha * INR n) (INR (first (M N)) * alpha)
     (- (INR (first (M N)) * alpha)));
 rewrite (Rplus_opp_r (INR (first (M N)) * alpha)).
 elim (Rplus_ne (alpha * INR n)); intros a b; rewrite a; clear a b;
  rewrite (Rmult_comm alpha (INR n)); fold (frac_part_n_alpha n) in |- *;
  intro; cut (0 < frac_part_n_alpha (first (M N)))%R.
intro;
 generalize
  (tech_Rgt_minus (frac_part_n_alpha n) (frac_part_n_alpha (first (M N))) H4);
 clear H4 H1 H2; intro; unfold Rgt in H1;
 generalize
  (Rgt_not_le (frac_part_n_alpha n)
     (frac_part_n_alpha n - frac_part_n_alpha (first (M N))) H1);
 auto with arith real.
fold (frac_part_n_alpha (first (M N)) > 0)%R in |- *;
 apply (fp_first_R0 alpha_irr prop_N (M N)).
unfold Rge in |- *; unfold Rgt in |- *;
 cut
  ((frac_part_n_alpha (first (M N)) < frac_part_n_alpha (n + first (M N)))%R \/
   frac_part_n_alpha (first (M N)) = frac_part_n_alpha (n + first (M N))).
intro; elim H2; intro.
left; auto with arith real.
right; auto with arith real.
fold
 (frac_part_n_alpha (first (M N)) <= frac_part_n_alpha (n + first (M N)))%R
 in |- *; apply (first_n (M N) (n + first (M N)));
 auto with arith real;
 generalize (plus_lt_compat_r n (last (M N)) (first (M N)) H0);
 intro; unfold M at 2 in |- *;
 rewrite (first_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real;
 rewrite (last_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real; rewrite (plus_comm (first (M N)) (last (M N)));
 assumption.
intro; elim H1; intros; elim H2; intros; elim H4; intros; elim H6; intros;
 clear H6 H4 H2 H1.
elim (le_or_lt x n); intro.
generalize
 (Ropp_lt_gt_contravar (frac_part_n_alpha n) (frac_part_n_alpha x) H7);
 intro;
 generalize
  (Rplus_gt_compat_l (frac_part_n_alpha (n + first (M N)))
     (- frac_part_n_alpha n) (- frac_part_n_alpha x) H2);
 fold (frac_part_n_alpha (n + first (M N)) - frac_part_n_alpha n)%R in |- *;
 fold (frac_part_n_alpha (n + first (M N)) - frac_part_n_alpha x)%R in |- *;
 fold (frac_part_n_alpha (n + first (M N)) > frac_part_n_alpha x)%R in H8;
 generalize
  (Rgt_ge (frac_part_n_alpha (n + first (M N))) (frac_part_n_alpha x) H8);
 intro; unfold frac_part_n_alpha in H4; unfold frac_part_n_alpha in |- *;
 rewrite <- (Rminus_fp1 (INR (n + first (M N)) * alpha) (INR x * alpha) H4);
 fold (frac_part_n_alpha x > frac_part_n_alpha n)%R in H7;
 generalize
  (Rgt_trans (frac_part_n_alpha (n + first (M N)))
     (frac_part_n_alpha x) (frac_part_n_alpha n) H8 H7);
 intro;
 generalize
  (Rgt_ge (frac_part_n_alpha (n + first (M N))) (frac_part_n_alpha n) H6);
 intro; unfold frac_part_n_alpha in H9;
 rewrite <- (Rminus_fp1 (INR (n + first (M N)) * alpha) (INR n * alpha) H9);
 rewrite (plus_INR n (first (M N)));
 rewrite (Rmult_comm (INR n + INR (first (M N))) alpha);
 rewrite (Rmult_plus_distr_l alpha (INR n) (INR (first (M N))));
 rewrite (Rmult_comm alpha (INR n)); unfold Rminus at 1 in |- *;
 rewrite (Rplus_comm (INR n * alpha) (alpha * INR (first (M N))));
 rewrite
  (Rplus_assoc (alpha * INR (first (M N))) (INR n * alpha)
     (- (INR n * alpha))); rewrite (Rplus_opp_r (INR n * alpha));
 elim (Rplus_ne (alpha * INR (first (M N)))); intros a b;
 rewrite a; clear a b; rewrite (Rmult_comm alpha (INR (first (M N))));
 fold (frac_part_n_alpha (first (M N))) in |- *; unfold Rminus in |- *;
 rewrite
  (Rplus_assoc (INR (first (M N)) * alpha) (INR n * alpha)
     (- (INR x * alpha))); rewrite (Rmult_comm (INR (first (M N))) alpha);
 rewrite (Rmult_comm (INR n) alpha);
 rewrite <- (Ropp_mult_distr_l_reverse (INR x) alpha);
 rewrite (Rmult_comm (- INR x) alpha);
 rewrite <- (Rmult_plus_distr_l alpha (INR n) (- INR x));
 rewrite <- (Rmult_plus_distr_l alpha (INR (first (M N))) (INR n + - INR x));
 fold (INR n - INR x)%R in |- *; rewrite <- (minus_INR n x H1);
 rewrite <- (plus_INR (first (M N)) (n - x));
 rewrite (Rmult_comm alpha (INR (first (M N) + (n - x))));
 fold (frac_part_n_alpha (first (M N) + (n - x))) in |- *;
 intro; clear H2 H4 H6 H9; cut (0 < first (M N) + (n - x)).
cut (first (M N) + (n - x) < M N).
intros;
 generalize
  (first_n (M N) (first (M N) + (n - x)) (prop_N (M N)) H4 H2 prop_alpha);
 intro; clear H2 H4; unfold Rgt in H10;
 generalize
  (Rgt_not_le (frac_part_n_alpha (first (M N)))
     (frac_part_n_alpha (first (M N) + (n - x))) H10);
 auto with arith real.
unfold M at 2 in |- *;
 rewrite (first_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
apply (plus_lt_compat_l (n - x) (last N) (first (M N)));
 rewrite (last_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
apply (lt_minus_p n (last (M N)) x H0).
apply (lt_O_plus (first (M N)) (n - x) (first_0 (M N) (prop_N (M N)))).
generalize
 (Rplus_lt_compat_l (- frac_part_n_alpha n) (frac_part_n_alpha x)
    (frac_part_n_alpha (n + first (M N))) H8);
 rewrite (Rplus_comm (- frac_part_n_alpha n) (frac_part_n_alpha x));
 rewrite
  (Rplus_comm (- frac_part_n_alpha n) (frac_part_n_alpha (n + first (M N))))
  ; fold (frac_part_n_alpha x - frac_part_n_alpha n)%R in |- *;
 fold (frac_part_n_alpha (n + first (M N)) - frac_part_n_alpha n)%R in |- *;
 fold (frac_part_n_alpha x > frac_part_n_alpha n)%R in H7;
 generalize (Rgt_ge (frac_part_n_alpha x) (frac_part_n_alpha n) H7);
 intro;
 fold (frac_part_n_alpha (n + first (M N)) > frac_part_n_alpha x)%R in H8;
 generalize
  (Rgt_trans (frac_part_n_alpha (n + first (M N)))
     (frac_part_n_alpha x) (frac_part_n_alpha n) H8 H7);
 intro;
 generalize
  (Rgt_ge (frac_part_n_alpha (n + first (M N))) (frac_part_n_alpha n) H4);
 intro; unfold frac_part_n_alpha in H2, H6; unfold frac_part_n_alpha in |- *;
 rewrite <- (Rminus_fp1 (INR x * alpha) (INR n * alpha) H2);
 rewrite <- (Rminus_fp1 (INR (n + first (M N)) * alpha) (INR n * alpha) H6);
 rewrite (plus_INR n (first (M N)));
 rewrite (Rmult_comm (INR n + INR (first (M N))) alpha);
 rewrite (Rmult_plus_distr_l alpha (INR n) (INR (first (M N))));
 rewrite (Rmult_comm alpha (INR n));
 rewrite (Rmult_comm alpha (INR (first (M N)))); unfold Rminus at 2 in |- *;
 rewrite (Rplus_comm (INR n * alpha) (INR (first (M N)) * alpha));
 rewrite
  (Rplus_assoc (INR (first (M N)) * alpha) (INR n * alpha)
     (- (INR n * alpha))); rewrite (Rplus_opp_r (INR n * alpha));
 elim (Rplus_ne (INR (first (M N)) * alpha)); intros a b;
 rewrite a; clear a b; fold (frac_part_n_alpha (first (M N))) in |- *;
 clear H2 H4 H6; unfold Rminus in |- *; rewrite (Rmult_comm (INR x) alpha);
 rewrite <- (Ropp_mult_distr_l_reverse (INR n) alpha);
 rewrite (Rmult_comm (- INR n) alpha);
 rewrite <- (Rmult_plus_distr_l alpha (INR x) (- INR n));
 fold (INR x - INR n)%R in |- *; rewrite (Rmult_comm alpha (INR x - INR n));
 generalize (lt_le_weak n x H1); intro; rewrite <- (minus_INR x n H2);
 fold (frac_part_n_alpha (x - n)) in |- *; intro; cut (0 < x - n).
intro; cut (x - n < M N).
intro; generalize (first_n (M N) (x - n) (prop_N (M N)) H6 H9 prop_alpha);
 intro; clear H9 H6;
 generalize
  (Rgt_not_le (frac_part_n_alpha (first (M N))) (frac_part_n_alpha (x - n))
     H4); auto with arith real.
apply (lt_minus_p x (M N) n H5).
apply (lt_minus2 n x H1).
Qed.

Lemma inter31b :
 forall N n : nat,
 last (M N) <= n -> n < M N -> after (M N) n = n - last (M N).
intros; elim (le_lt_or_eq (last (M N)) n H); intro; clear H.
apply (sym_equal (x:=n - last (M N)) (y:=after (M N) n));
 apply (tech_after alpha_irr (M N) n (n - last (M N)));
 auto with arith real.
apply (lt_trans 0 (last (M N)) n (last_0 (M N) (prop_N (M N))) H1).
apply (lt_minus_p n (M N) (last (M N)) H0).
cut
 (frac_part_n_alpha n <
  frac_part_n_alpha n - frac_part_n_alpha (last (M N)) + 1)%R.
intro; unfold frac_part_n_alpha in H; generalize H; clear H;
 rewrite <- (Rminus_fp2 (INR n * alpha) (INR (last (M N)) * alpha)).
fold (frac_part_n_alpha n) in |- *; rewrite (Rmult_comm (INR n) alpha);
 unfold Rminus in |- *;
 rewrite <- (Ropp_mult_distr_l_reverse (INR (last (M N))) alpha);
 rewrite (Rmult_comm (- INR (last (M N))) alpha);
 rewrite <- (Rmult_plus_distr_l alpha (INR n) (- INR (last (M N))));
 fold (INR n - INR (last (M N)))%R in |- *;
 rewrite <- (minus_INR n (last (M N)) (lt_le_weak (last (M N)) n H1));
 rewrite (Rmult_comm alpha (INR (n - last (M N))));
 fold (frac_part_n_alpha (n - last (M N))) in |- *;
 trivial.
fold (frac_part_n_alpha n) in |- *;
 fold (frac_part_n_alpha (last (M N))) in |- *;
 generalize
  (last_n (M N) n (prop_N (M N))
     (lt_trans 0 (last (M N)) n (last_0 (M N) (prop_N (M N))) H1) H0
     prop_alpha); intro; unfold Rle in H; elim H; intro;
 auto with arith real.
generalize
 (contra_tech_fp_alp_irr alpha_irr prop_alpha (last (M N)) n
    (lt_not_eq (last (M N)) n H1)); intro; elimtype False;
 auto with arith real.
unfold Rminus in |- *;
 rewrite
  (Rplus_assoc (frac_part_n_alpha n) (- frac_part_n_alpha (last (M N))) 1)
  ; rewrite (Rplus_comm (- frac_part_n_alpha (last (M N))) 1);
 fold (1 - frac_part_n_alpha (last (M N)))%R in |- *;
 elim (Rplus_ne (frac_part_n_alpha n)); intros a b;
 pattern (frac_part_n_alpha n) at 1 in |- *; rewrite <- a;
 clear a b;
 apply
  (Rplus_lt_compat_l (frac_part_n_alpha n) 0
     (1 - frac_part_n_alpha (last (M N))));
 fold (1 - frac_part_n_alpha (last (M N)) > 0)%R in |- *;
 apply (Rgt_minus 1 (frac_part_n_alpha (last (M N))));
 unfold Rgt in |- *; unfold frac_part_n_alpha in |- *;
 elim (base_fp (INR (last (M N)) * alpha)); intros;
 assumption.
intro; elim H; intros; elim H2; intros; elim H4; intros; elim H6; intros;
 clear H H2 H4 H6.
elim (le_or_lt n x); intro.
generalize
 (Rplus_lt_compat_l (- frac_part_n_alpha (n - last (M N)))
    (frac_part_n_alpha n) (frac_part_n_alpha x) H7);
 intro;
 generalize
  (Rplus_lt_compat_l 1
     (- frac_part_n_alpha (n - last (M N)) + frac_part_n_alpha n)
     (- frac_part_n_alpha (n - last (M N)) + frac_part_n_alpha x) H2);
 clear H2;
 rewrite
  (Rplus_comm 1 (- frac_part_n_alpha (n - last (M N)) + frac_part_n_alpha n))
  ;
 rewrite
  (Rplus_comm 1 (- frac_part_n_alpha (n - last (M N)) + frac_part_n_alpha x))
  ;
 rewrite
  (Rplus_comm (- frac_part_n_alpha (n - last (M N))) (frac_part_n_alpha n))
  ;
 rewrite
  (Rplus_comm (- frac_part_n_alpha (n - last (M N))) (frac_part_n_alpha x))
  ; fold (frac_part_n_alpha n - frac_part_n_alpha (n - last (M N)))%R in |- *;
 fold (frac_part_n_alpha x - frac_part_n_alpha (n - last (M N)))%R in |- *;
 unfold frac_part_n_alpha in |- *;
 rewrite <- (Rminus_fp2 (INR n * alpha) (INR (n - last (M N)) * alpha)).
rewrite <- (Rminus_fp2 (INR x * alpha) (INR (n - last (M N)) * alpha)).
rewrite (minus_INR n (last (M N)) (lt_le_weak (last (M N)) n H1));
 unfold Rminus in |- *;
 rewrite (Rmult_comm (INR n + - INR (last (M N))) alpha);
 rewrite (Rmult_plus_distr_l alpha (INR n) (- INR (last (M N))));
 rewrite (Ropp_plus_distr (alpha * INR n) (alpha * - INR (last (M N))));
 rewrite <-
  (Rplus_assoc (INR n * alpha) (- (alpha * INR n))
     (- (alpha * - INR (last (M N))))); rewrite (Rmult_comm (INR n) alpha);
 rewrite (Rplus_opp_r (alpha * INR n));
 elim (Rplus_ne (- (alpha * - INR (last (M N)))));
 intros a b; rewrite b; clear a b;
 rewrite (Rmult_comm alpha (- INR (last (M N))));
 rewrite <- (Ropp_mult_distr_l_reverse (- INR (last (M N))) alpha);
 rewrite (Ropp_involutive (INR (last (M N))));
 fold (frac_part_n_alpha (last (M N))) in |- *;
 rewrite <-
  (Rplus_assoc (INR x * alpha) (- (alpha * INR n)) (INR (last (M N)) * alpha))
  ; rewrite (Rmult_comm alpha (INR n));
 rewrite <- (Ropp_mult_distr_l_reverse (INR n) alpha);
 rewrite (Rmult_comm (- INR n) alpha); rewrite (Rmult_comm (INR x) alpha);
 rewrite <- (Rmult_plus_distr_l alpha (INR x) (- INR n));
 fold (INR x - INR n)%R in |- *; rewrite <- (minus_INR x n H);
 rewrite (Rmult_comm (INR (last (M N))) alpha);
 rewrite <- (Rmult_plus_distr_l alpha (INR (x - n)) (INR (last (M N))));
 rewrite <- (plus_INR (x - n) (last (M N)));
 rewrite (Rmult_comm alpha (INR (x - n + last (M N))));
 fold (frac_part_n_alpha (x - n + last (M N))) in |- *;
 intro; cut (0 < x - n + last (M N)).
intro; cut (x - n + last (M N) < M N).
intro;
 generalize
  (last_n (M N) (x - n + last (M N)) (prop_N (M N)) H4 H6 prop_alpha);
 intro; clear H4 H6;
 generalize
  (Rgt_not_le (frac_part_n_alpha (x - n + last (M N)))
     (frac_part_n_alpha (last (M N))) H2); intro; elimtype False;
 auto with arith real.
apply (tech_inter31b (last (M N)) n x (M N) H1 H H5).
rewrite plus_comm;
 apply (lt_O_plus (last (M N)) (x - n) (last_0 (M N) (prop_N (M N)))).
fold (frac_part_n_alpha x) in |- *;
 fold (frac_part_n_alpha (n - last (M N))) in |- *;
 assumption.
fold (frac_part_n_alpha n) in |- *;
 fold (frac_part_n_alpha (n - last (M N))) in |- *;
 apply
  (Rlt_trans (frac_part_n_alpha n) (frac_part_n_alpha x)
     (frac_part_n_alpha (n - last (M N))) H7 H8).
generalize
 (Ropp_lt_gt_contravar (frac_part_n_alpha x)
    (frac_part_n_alpha (n - last (M N))) H8); unfold Rgt in |- *;
 intro;
 generalize
  (Rplus_lt_compat_l (frac_part_n_alpha n)
     (- frac_part_n_alpha (n - last (M N))) (- frac_part_n_alpha x) H2);
 clear H2;
 fold (frac_part_n_alpha n - frac_part_n_alpha (n - last (M N)))%R in |- *;
 fold (frac_part_n_alpha n - frac_part_n_alpha x)%R in |- *;
 intro;
 generalize
  (Rplus_lt_compat_l 1
     (frac_part_n_alpha n - frac_part_n_alpha (n - last (M N)))
     (frac_part_n_alpha n - frac_part_n_alpha x) H2);
 clear H2;
 rewrite
  (Rplus_comm 1 (frac_part_n_alpha n - frac_part_n_alpha (n - last (M N))))
  ; rewrite (Rplus_comm 1 (frac_part_n_alpha n - frac_part_n_alpha x));
 unfold frac_part_n_alpha in |- *;
 rewrite <- (Rminus_fp2 (INR n * alpha) (INR (n - last (M N)) * alpha)).
rewrite <- (Rminus_fp2 (INR n * alpha) (INR x * alpha)).
rewrite (Rmult_comm (INR n) alpha); unfold Rminus at 2 in |- *;
 rewrite <- (Ropp_mult_distr_l_reverse (INR x) alpha);
 rewrite (Rmult_comm (- INR x) alpha);
 rewrite <- (Rmult_plus_distr_l alpha (INR n) (- INR x));
 fold (INR n - INR x)%R in |- *;
 rewrite <- (minus_INR n x (lt_le_weak x n H));
 rewrite (Rmult_comm alpha (INR (n - x)));
 fold (frac_part_n_alpha (n - x)) in |- *;
 rewrite (minus_INR n (last (M N)) (lt_le_weak (last (M N)) n H1));
 unfold Rminus in |- *;
 rewrite (Rmult_comm (INR n + - INR (last (M N))) alpha);
 rewrite (Rmult_plus_distr_l alpha (INR n) (- INR (last (M N))));
 rewrite (Ropp_plus_distr (alpha * INR n) (alpha * - INR (last (M N))));
 rewrite <-
  (Rplus_assoc (alpha * INR n) (- (alpha * INR n))
     (- (alpha * - INR (last (M N))))); rewrite (Rplus_opp_r (alpha * INR n));
 elim (Rplus_ne (- (alpha * - INR (last (M N)))));
 intros a b; rewrite b; clear a b;
 rewrite (Rmult_comm alpha (- INR (last (M N))));
 rewrite <- (Ropp_mult_distr_l_reverse (- INR (last (M N))) alpha);
 rewrite (Ropp_involutive (INR (last (M N))));
 fold (frac_part_n_alpha (last (M N))) in |- *; intro;
 cut (0 < n - x).
intro; cut (n - x < M N).
intro; generalize (last_n (M N) (n - x) (prop_N (M N)) H4 H6 prop_alpha);
 intro;
 generalize
  (Rgt_not_le (frac_part_n_alpha (n - x)) (frac_part_n_alpha (last (M N))) H2);
 intro; elimtype False; auto with arith real.
apply (lt_minus_p n (M N) x H0).
apply (lt_minus2 x n H).
fold (frac_part_n_alpha n) in |- *; fold (frac_part_n_alpha x) in |- *;
 assumption.
fold (frac_part_n_alpha n) in |- *;
 fold (frac_part_n_alpha (n - last (M N))) in |- *;
 apply
  (Rlt_trans (frac_part_n_alpha n) (frac_part_n_alpha x)
     (frac_part_n_alpha (n - last (M N))) H7 H8).
rewrite <- H1; rewrite <- (minus_n_n (last (M N)));
 apply (after_last prop_alpha prop_N (M N)).
Qed.

Lemma tech1 :
 forall N n : nat,
 N - first N <= n ->
 n < last N ->
 (frac_part_n_alpha n < frac_part_n_alpha (n + first N - last N))%R.
intros; cut (frac_part_n_alpha n < frac_part_n_alpha (n + first N))%R.
intro;
 cut
  (frac_part_n_alpha (n + first N) < frac_part_n_alpha (n + first N - last N))%R.
intro;
 apply
  (Rlt_trans (frac_part_n_alpha n) (frac_part_n_alpha (n + first N))
     (frac_part_n_alpha (n + first N - last N)) H1 H2).
cut (0 < n + first N).
cut (n + first N < M N).
intros;
 apply (tech_after_lt (M N) (n + first N) (n + first N - last N) H3 H2).
apply (lt_minus_not (last N) (n + first N)).
generalize (le_minus_plus N (first N) n H); intro;
 apply (lt_le_trans (last N) N (n + first N) (last_N N (prop_N N)) H4).
rewrite (last_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
generalize H2; clear H2;
 rewrite (first_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
intro; cut (last (M N) <= n + first (M N)).
intro; apply (inter31b N (n + first (M N)) H4 H2).
rewrite <- (last_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
rewrite <- (first_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
generalize (le_minus_plus N (first N) n H); intro;
 apply (le_trans (last N) N (n + first N) (last_N01 N) H4).
unfold M in |- *; rewrite (plus_comm (first N) (last N));
 apply (plus_lt_compat_r n (last N) (first N) H0).
generalize (le_minus_plus N (first N) n H); intro; cut (0 < N).
intro; apply (lt_le_trans 0 N (n + first N) H3 H2).
apply (arith_2_0 N (prop_N N)).
cut (0 < n).
cut (n < M N).
intros; apply (tech_after_lt (M N) n (n + first N) H2 H1).
generalize (lt_O_plus n (first N) H2); intro; apply Compare.not_eq_sym;
 red in |- *; intro; apply (lt_not_eq 0 (n + first N) H3 H4).
rewrite (first_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
generalize H0; rewrite (last_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real; clear H0; intro; apply (inter31a N n H2 H0).
generalize (lt_trans n (last N) N H0 (last_N N (prop_N N))); intro;
 unfold M in |- *; cut (N <= first N + last N).
intro; apply (lt_le_trans n N (first N + last N) H1 H2).
apply (le_N_M alpha_irr prop_alpha prop_N N (M N)); auto with arith real.
apply
 (lt_le_trans 0 (N - first N) n
    (lt_minus2 (first N) N (first_N N (prop_N N))) H).
Qed.

Lemma tech_suc_N :
 forall N n : nat,
 0 < n ->
 n < N ->
 forall 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 (after N n) ->
 (frac_part_n_alpha (after N n) < frac_part_n_alpha k)%R.
unfold after in |- *; intros; generalize H4; clear H4;
 case (exist_after_M (frac_part_n_alpha n) (P1 n) (P2 n) N);
 intro.
elim s; intros x y H4; clear s; elim y; intros; clear y; unfold Rgt in H6;
 cut (0 <= k).
elim H6; intros; elim H8; intros; generalize (H11 k H9 H2 H3);
 unfold Rge in |- *; unfold Rgt in |- *; intro; elim H12;
 auto with arith real.
intro; elimtype False; auto with arith real.
apply (lt_le_weak 0 k H1).
unfold frac_part_n_alpha in |- *; simpl in |- *; rewrite Rmult_0_l;
 rewrite fp_R0; elim (base_fp (INR k * alpha)); intros;
 unfold Rge in H4; elim H4; auto with arith real.
intro; elimtype False; auto with arith real.
Qed.

Lemma tech_suc_M :
 forall N n : nat,
 N - first N <= n ->
 n < last N ->
 (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 (n + first N - last N))%R) ->
 False.
intros; elim H1; intros; clear H1.
elim H2; intros; elim H3; intros; clear H3; clear H2; elim H5; intros;
 clear H5.
cut (0 < n).
intro; cut (n < M N).
intros; cut (x < M N).
intro;
 elim (Rtotal_order (frac_part_n_alpha x) (frac_part_n_alpha (n + first N)));
 intro.
cut (n + first N = after (M N) n).
intro; rewrite H9 in H8;
 cut (frac_part_n_alpha x <> frac_part_n_alpha (after (M N) n)).
intro; generalize (tech_suc_N (M N) n H5 H6 x H1 H7 H2 H10).
intro;
 generalize
  (Rlt_asym (frac_part_n_alpha x) (frac_part_n_alpha (after (M N) n)) H8).
intro; auto with arith real.
apply
 (Rlt_dichotomy_converse (frac_part_n_alpha x)
    (frac_part_n_alpha (after (M N) n))).
left; auto with arith real.
apply sym_equal.
rewrite (first_eq_M_N alpha_irr prop_alpha prop_N N (M N)).
apply (inter31a N n H5).
rewrite <- (last_eq_M_N alpha_irr prop_alpha prop_N N (M N)).
assumption.
auto with arith real.
auto with arith real.
elim H8; intro; clear H8.
cut (x <> n + first N).
intro;
 generalize (contra_tech_fp_alp_irr alpha_irr prop_alpha x (n + first N) H8);
 auto with arith real.
cut (x < n + first N).
intro; red in |- *; intro; apply (lt_not_eq x (n + first N) H8); assumption.
generalize (le_minus_plus N (first N) n H); intro;
 apply (lt_le_trans x N (n + first N) H4 H8).
cut (0 < n + first (M N)).
intro; cut (n + first (M N) < M N).
intro;
 cut
  (frac_part_n_alpha x <> frac_part_n_alpha (after (M N) (n + first (M N)))).
intro; unfold Rgt in H9;
 rewrite
  (first_eq_M_N alpha_irr prop_alpha prop_N N (M N)
     (refl_equal (first N + last N))) in H9;
 generalize (tech_suc_N (M N) (n + first (M N)) H8 H10 x H1 H7 H9 H11);
 intro; cut (last (M N) <= n + first (M N)).
intro; rewrite (inter31b N (n + first (M N)) H13 H10) in H12.
rewrite
 (first_eq_M_N alpha_irr prop_alpha prop_N N (M N)
    (refl_equal (first N + last N))) in H3;
 rewrite
  (last_eq_M_N alpha_irr prop_alpha prop_N N (M N)
     (refl_equal (first N + last N))) in H3;
 generalize
  (Rlt_asym (frac_part_n_alpha (n + first (M N) - last (M N)))
     (frac_part_n_alpha x) H12); intro; auto with arith real.
generalize (le_minus_plus N (first N) n H); intro.
generalize (last_N01 N); intro.
rewrite <-
 (first_eq_M_N alpha_irr prop_alpha prop_N N (M N)
    (refl_equal (first N + last N)));
 rewrite <-
  (last_eq_M_N alpha_irr prop_alpha prop_N N (M N)
     (refl_equal (first N + last N)));
 apply (le_trans (last N) N (n + first N) H14 H13).
cut (last (M N) <= n + first (M N)).
intro; rewrite (inter31b N (n + first (M N)) H11 H10);
 rewrite <-
  (first_eq_M_N alpha_irr prop_alpha prop_N N (M N)
     (refl_equal (first N + last N)));
 rewrite <-
  (last_eq_M_N alpha_irr prop_alpha prop_N N (M N)
     (refl_equal (first N + last N)));
 apply
  (Rlt_dichotomy_converse (frac_part_n_alpha x)
     (frac_part_n_alpha (n + first N - last N))).
left; assumption.
generalize (le_minus_plus N (first N) n H); intro.
generalize (last_N01 N); intro;
 rewrite <-
  (first_eq_M_N alpha_irr prop_alpha prop_N N (M N)
     (refl_equal (first N + last N)));
 rewrite <-
  (last_eq_M_N alpha_irr prop_alpha prop_N N (M N)
     (refl_equal (first N + last N)));
 apply (le_trans (last N) N (n + first N) H12 H11).
rewrite <-
 (first_eq_M_N alpha_irr prop_alpha prop_N N (M N)
    (refl_equal (first N + last N))); unfold M in |- *;
 rewrite (plus_comm (first N) (last N));
 apply (plus_lt_compat_r n (last N) (first N) H0).
apply (lt_O_plus n (first (M N)) H5).
cut (N <= M N).
intro; apply (lt_le_trans x N (M N) H4 H7).
apply
 (le_N_M alpha_irr prop_alpha prop_N N (M N) (refl_equal (first N + last N))).
cut (last N < N).
intro; cut (N <= M N).
intro; generalize (lt_trans n (last N) N H0 H6).
intro; apply (lt_le_trans n N (M N) H8 H7).
apply
 (le_N_M alpha_irr prop_alpha prop_N N (M N) (refl_equal (first N + last N))).
apply (last_N N (prop_N N)).
cut (0 < N - first N).
intro; apply (lt_le_trans 0 (N - first N) n H5 H).
apply (lt_minus2 (first N) N (first_N N (prop_N N))).
Qed.

Lemma tech_suc_M1 :
 forall N n : nat,
 N - first N <= n ->
 n < last N ->
 forall 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 (n + first N - last N))%R).
intros; generalize (tech_suc_M N n H H0); intro; red in |- *; intro; apply H1;
 split with k; auto with arith real.
Qed.

Lemma eq_after_M_N1 :
 forall N n : nat, 0 < n -> n < N - first N -> after (M N) n = after N n.
intros; cut (n < last (M N)).
intro; generalize (inter31a N n H H1);
 rewrite <-
  (first_eq_M_N alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))
  ; intro; apply (tech_fp_alp_irr alpha_irr (after (M N) n) (after N n));
 apply
  (Rge_antisym (frac_part_n_alpha (after (M N) n))
     (frac_part_n_alpha (after N n))).
apply
 (Rnot_lt_ge (frac_part_n_alpha (after (M N) n))
    (frac_part_n_alpha (after N n))); red in |- *;
 intro; cut (0 < after (M N) n).
intro; cut (after (M N) n < N).
intro; cut (frac_part_n_alpha n < frac_part_n_alpha (after (M N) n))%R.
intro;
 generalize
  (tech_suc_N N n H (contra_lt_minus_p n N (first N) H0)
     (after (M N) n) H4 H5 H6
     (Rlt_dichotomy_converse (frac_part_n_alpha (after (M N) n))
        (frac_part_n_alpha (after N n))
        (or_introl
           (frac_part_n_alpha (after (M N) n) > frac_part_n_alpha (after N n))%R
           H3))); intro;
 generalize
  (Rlt_asym (frac_part_n_alpha (after (M N) n))
     (frac_part_n_alpha (after N n)) H3); intro; elimtype False;
 auto with arith real.
apply
 (tech_after_lt (M N) n (after (M N) n) H
    (lt_le_trans n N (M N) (contra_lt_minus_p n N (first N) H0)
       (le_N_M alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))));
 auto with arith real.
rewrite H2; red in |- *; intro; apply (lt_O_plus_eq n (first N) H);
 auto with arith real.
rewrite H2; apply (lt_n_minus_plus n N (first N) H0).
rewrite H2; apply (lt_O_plus n (first N) H).
apply
 (Rnot_lt_ge (frac_part_n_alpha (after N n))
    (frac_part_n_alpha (after (M N) n))); red in |- *;
 intro; apply (prop_after (M N) n (after (M N) n));
 auto with arith real.
split with (after N n); split.
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; assumption.
intro; generalize (a (last N) (le_O_n (last N)) (last_N N (prop_N N))); intro;
 elim H4; intros; clear a H4;
 generalize
  (last_n N n (prop_N N) H (contra_lt_minus_p n N (first N) H0) prop_alpha);
 intro; cut (frac_part_n_alpha n = frac_part_n_alpha (last N)).
intro; generalize (tech_fp_alp_irr alpha_irr n (last N) H7);
 rewrite (last_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
intro; generalize (lt_not_eq n (last (M N)) H1); intro; elimtype False;
 auto with arith real.
elim (Rle_le_eq (frac_part_n_alpha n) (frac_part_n_alpha (last N))); intros;
 clear H8; apply H7; auto with arith real.
split.
cut (after N n < N).
intro;
 apply
  (lt_le_trans (after N n) N (M N) H4
     (le_N_M alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))).
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; elim H5; intros; assumption.
intro; apply (arith_2_0 N (prop_N N)).
split; auto with arith real.
apply (tech_after_lt N n (after N n) H (contra_lt_minus_p n N (first N) H0));
 auto with arith real.
red in |- *; unfold after in |- *;
 case (exist_after_M (frac_part_n_alpha n) (P1 n) (P2 n) N).
intro; elim s; intros x y H4; elim y; intros; generalize (lt_not_eq 0 x H5);
 intro; auto with arith real.
intros; generalize (a (last N) (le_O_n (last N)) (last_N N (prop_N N)));
 intro; elim H5; intros; clear a H5;
 generalize
  (last_n N n (prop_N N) H (contra_lt_minus_p n N (first N) H0) prop_alpha);
 intro; cut (frac_part_n_alpha n = frac_part_n_alpha (last N)).
intro; generalize (tech_fp_alp_irr alpha_irr n (last N) H8);
 rewrite (last_eq_M_N alpha_irr prop_alpha prop_N N (M N));
 auto with arith real.
intro; generalize (lt_not_eq n (last (M N)) H1); intro; elimtype False;
 auto with arith real.
elim (Rle_le_eq (frac_part_n_alpha n) (frac_part_n_alpha (last N))); intros;
 clear H9; apply H8; auto with arith real.
cut (N - first N <= last (M N)).
intro; apply (lt_le_trans n (N - first N) (last (M N)) H0 H1).
generalize (le_N_M alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)));
 unfold M at 1 in |- *;
 rewrite <-
  (last_eq_M_N alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))
  ; intro; apply (le_plus_min N (first N) (last N) H1).
Qed.

Lemma eq_after_M_N2 :
 forall N n : nat, last N <= n -> n < N -> after (M N) n = after N n.
intros; generalize (le_lt_or_eq (last N) n H); intro; elim H1; intro;
 clear H1.
rewrite (last_eq_M_N alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))
  in H;
 generalize
  (inter31b N n H
     (lt_le_trans n N (M N) H0
        (le_N_M alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))));
 rewrite <-
  (last_eq_M_N alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))
  ; intro; apply (tech_fp_alp_irr alpha_irr (after (M N) n) (after N n));
 apply
  (Rge_antisym (frac_part_n_alpha (after (M N) n))
     (frac_part_n_alpha (after N n))).
apply
 (Rnot_lt_ge (frac_part_n_alpha (after (M N) n))
    (frac_part_n_alpha (after N n))); red in |- *;
 intro; cut (0 < after (M N) n).
intro; cut (after (M N) n < N).
intro; cut (frac_part_n_alpha n < frac_part_n_alpha (after (M N) n))%R.
intro;
 generalize
  (tech_suc_N N n (lt_trans 0 (last N) n (last_0 N (prop_N N)) H2) H0
     (after (M N) n) H4 H5 H6
     (Rlt_dichotomy_converse (frac_part_n_alpha (after (M N) n))
        (frac_part_n_alpha (after N n))
        (or_introl
           (frac_part_n_alpha (after (M N) n) > frac_part_n_alpha (after N n))%R
           H3))); intro;
 generalize
  (Rlt_asym (frac_part_n_alpha (after (M N) n))
     (frac_part_n_alpha (after N n)) H3); intro; elimtype False;
 auto with arith real.
apply
 (tech_after_lt (M N) n (after (M N) n)
    (lt_trans 0 (last N) n (last_0 N (prop_N N)) H2)
    (lt_le_trans n N (M N) H0
       (le_N_M alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))));
 auto with arith real.
rewrite H1; red in |- *; intro; apply (lt_minus_not (last N) n H2);
 auto with arith real.
rewrite H1; apply (lt_minus_p n N (last N) H0).
rewrite H1; apply (lt_minus2 (last N) n H2).
apply
 (Rnot_lt_ge (frac_part_n_alpha (after N n))
    (frac_part_n_alpha (after (M N) n))); red in |- *;
 intro; apply (prop_after (M N) n (after (M N) n));
 auto with arith real.
split with (after N n); split.
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; assumption.
intro; generalize (a (last N) (le_O_n (last N)) (last_N N (prop_N N))); intro;
 elim H4; intros; clear a H4;
 generalize
  (last_n N n (prop_N N) (lt_trans 0 (last N) n (last_0 N (prop_N N)) H2) H0
     prop_alpha); intro;
 cut (frac_part_n_alpha n = frac_part_n_alpha (last N)).
intro; generalize (tech_fp_alp_irr alpha_irr n (last N) H7).
intro; generalize (lt_not_eq (last N) n H2); intro; elimtype False;
 auto with arith real.
elim (Rle_le_eq (frac_part_n_alpha n) (frac_part_n_alpha (last N))); intros;
 clear H8; apply H7; auto with arith real.
split.
cut (after N n < N).
intro;
 apply
  (lt_le_trans (after N n) N (M N) H4
     (le_N_M alpha_irr prop_alpha prop_N N (M N) (refl_equal (M N)))).
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; elim H5; intros; assumption.
intro; apply (arith_2_0 N (prop_N N)).
split; auto with arith real.
apply
 (tech_after_lt N n (after N n)
    (lt_trans 0 (last N) n (last_0 N (prop_N N)) H2) H0);
 auto with arith real.
red in |- *; unfold after in |- *;
 case (exist_after_M (frac_part_n_alpha n) (P1 n) (P2 n) N).
intro; elim s; intros x y H4; elim y; intros; generalize (lt_not_eq 0 x H5);
 intro; auto with arith real.
intros; generalize (a (last N) (le_O_n (last N)) (last_N N (prop_N N)));
 intro; elim H5; intros; clear a H5;
 generalize
  (last_n N n (prop_N N) (lt_trans 0 (last N) n (last_0 N (prop_N N)) H2) H0
     prop_alpha); intro;
 cut (frac_part_n_alpha n = frac_part_n_alpha (last N)).
intro; generalize (tech_fp_alp_irr alpha_irr n (last N) H8); intro;
 generalize (lt_not_eq (last N) n H2); intro; auto with arith real.
elim (Rle_le_eq (frac_part_n_alpha n) (frac_part_n_alpha (last N))); intros;
 clear H9; apply H8; auto with arith real.
rewrite <- H2; rewrite (after_last prop_alpha prop_N N);
 rewrite
  (last_eq_M_N alpha_irr prop_alpha prop_N N (M N)
     (refl_equal (first N + last N))); auto with arith real;
 rewrite (after_last prop_alpha prop_N (M N)); trivial.
Qed.

End particular.