(****************************************************************************
                                                                             
          IEEE754  :  FSucc                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export List.
Require Export Fnorm.
Section suc.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
 
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionNotZero : precision <> 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Definition FSucc (x : float) :=
  match Z_eq_bool (Fnum x) (pPred (vNum b)) with
  | true => Float (nNormMin radix precision) (Zsucc (Fexp x))
  | false =>
      match Z_eq_bool (Fnum x) (- nNormMin radix precision) with
      | true =>
          match Z_eq_bool (Fexp x) (- dExp b) with
          | true => Float (Zsucc (Fnum x)) (Fexp x)
          | false => Float (- pPred (vNum b)) (Zpred (Fexp x))
          end
      | false => Float (Zsucc (Fnum x)) (Fexp x)
      end
  end.
 
Theorem FSuccSimpl1 :
 forall x : float,
 Fnum x = pPred (vNum b) ->
 FSucc x = Float (nNormMin radix precision) (Zsucc (Fexp x)).
(* Goal: forall (x : float) (_ : @eq Z (Fnum x) (pPred (vNum b))), @eq float (FSucc x) (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
intros x H'; unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum x) (pPred (vNum b)));
 case (Z_eq_bool (Fnum x) (pPred (vNum b))); auto.
(* Goal: forall _ : not (@eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (Fnum x) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum x)) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Fnum x)) (Fexp x)) (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
intros H'0; Contradict H'0; auto.
Qed.
 
Theorem FSuccSimpl2 :
 forall x : float,
 Fnum x = (- nNormMin radix precision)%Z ->
 Fexp x <> (- dExp b)%Z ->
 FSucc x = Float (- pPred (vNum b)) (Zpred (Fexp x)).
(* Goal: forall (x : float) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))), @eq float (FSucc x) (Float (Z.succ (Fnum x)) (Fexp x)) *)
intros x H' H'0; unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum x) (pPred (vNum b)));
 case (Z_eq_bool (Fnum x) (pPred (vNum b))); auto.
(* Goal: forall _ : @eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)), @eq float (Float (nNormMin radix precision) (Z.succ (Z.opp (Z.of_N (dExp b))))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
intros H'1; absurd (0%nat <= pPred (vNum b))%Z; auto with zarith arith.
(* Goal: not (Z.le (Z.of_nat O) (pPred (vNum b))) *)
(* Goal: Z.le (Z.of_nat O) (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (Fnum x) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum x)) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Fnum x)) (Fexp x)) (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) *)
rewrite <- H'1; rewrite H'.
(* Goal: not (Z.le (Z.of_nat O) (Z.opp (nNormMin radix precision))) *)
(* Goal: Z.le (Z.of_nat O) (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
unfold nNormMin in |- *; simpl in |- *; auto with zarith.
(* Goal: not (Z.le Z0 (Z.opp (Zpower_nat radix (Init.Nat.pred precision)))) *)
(* Goal: Z.le (Z.of_nat O) (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
replace 0%Z with (- (0))%Z; auto with zarith.
(* Goal: Z.le (Z.of_nat O) (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
unfold pPred in |- *; apply Zle_Zpred; auto with zarith.
intros H'1;
 generalize (Z_eq_bool_correct (Fnum x) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum x) (- nNormMin radix precision)).
intros H'2; generalize (Z_eq_bool_correct (Fexp x) (- dExp b));
 case (Z_eq_bool (Fexp x) (- dExp b)); auto.
(* Goal: forall _ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))), @eq float (Float (Z.succ (Fnum x)) (Fexp x)) (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))), @eq float (Float (Z.succ (Fnum x)) (Fexp x)) (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) *)
intros H'3; Contradict H'0; auto.
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))), @eq float (Float (Z.succ (Fnum x)) (Fexp x)) (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) *)
intros H'2; Contradict H'2; auto.
Qed.
 
Theorem FSuccSimpl3 :
 FSucc (Float (- nNormMin radix precision) (- dExp b)) =
 Float (Zsucc (- nNormMin radix precision)) (- dExp b).
(* Goal: @eq float (FSucc (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
unfold FSucc in |- *; simpl in |- *.
generalize (Z_eq_bool_correct (- nNormMin radix precision) (pPred (vNum b)));
 case (Z_eq_bool (- nNormMin radix precision) (pPred (vNum b))); 
 auto.
(* Goal: forall _ : @eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)), @eq float (Float (nNormMin radix precision) (Z.succ (Z.opp (Z.of_N (dExp b))))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
intros H'1; absurd (0%nat <= pPred (vNum b))%Z; auto with zarith arith.
(* Goal: not (Z.le (Z.of_nat O) (pPred (vNum b))) *)
(* Goal: Z.le (Z.of_nat O) (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
rewrite <- H'1.
(* Goal: not (Z.le (Z.of_nat O) (Z.opp (nNormMin radix precision))) *)
(* Goal: Z.le (Z.of_nat O) (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
unfold nNormMin in |- *; simpl in |- *; auto with zarith.
(* Goal: not (Z.le Z0 (Z.opp (Zpower_nat radix (Init.Nat.pred precision)))) *)
(* Goal: Z.le (Z.of_nat O) (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
replace 0%Z with (- (0))%Z; auto with zarith.
(* Goal: Z.le (Z.of_nat O) (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))), @eq float (if Z_eq_bool (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
unfold pPred in |- *; apply Zle_Zpred; auto with zarith.
intros H';
 generalize
  (Z_eq_bool_correct (- nNormMin radix precision)
     (- nNormMin radix precision));
 case (Z_eq_bool (- nNormMin radix precision) (- nNormMin radix precision)).
intros H'0; generalize (Z_eq_bool_correct (- dExp b) (- dExp b));
 case (Z_eq_bool (- dExp b) (- dExp b)); auto.
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
intros H'1; Contradict H'1; auto.
(* Goal: forall _ : not (@eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
intros H'1; Contradict H'1; auto.
Qed.
 
Theorem FSuccSimpl4 :
 forall x : float,
 Fnum x <> pPred (vNum b) ->
 Fnum x <> (- nNormMin radix precision)%Z ->
 FSucc x = Float (Zsucc (Fnum x)) (Fexp x).
(* Goal: forall (x : float) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))), @eq float (FSucc x) (Float (Z.succ (Fnum x)) (Fexp x)) *)
intros x H' H'0; unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum x) (pPred (vNum b)));
 case (Z_eq_bool (Fnum x) (pPred (vNum b))); auto.
(* Goal: forall _ : @eq Z (Fnum x) (pPred (vNum b)), @eq float (Float (nNormMin radix precision) (Z.succ (Fexp x))) (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (Fnum x) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum x)) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Fnum x)) (Fexp x)) (Float (Z.succ (Fnum x)) (Fexp x)) *)
intros H'1; Contradict H'; auto.
intros H'1;
 generalize (Z_eq_bool_correct (Fnum x) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum x) (- nNormMin radix precision)); 
 auto.
(* Goal: forall _ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision)), @eq float (if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum x)) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) (Float (Z.succ (Fnum x)) (Fexp x)) *)
intros H'2; Contradict H'0; auto.
Qed.
 
Theorem FSuccDiff1 :
 forall x : float,
 Fnum x <> (- nNormMin radix precision)%Z ->
 Fminus radix (FSucc x) x = Float 1%nat (Fexp x) :>R.
(* Goal: forall (x : float) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
intros x H'.
generalize (Z_eq_bool_correct (Fnum x) (pPred (vNum b)));
 case (Z_eq_bool (Fnum x) (pPred (vNum b))); intros H'1.
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite FSuccSimpl1; auto.
(* Goal: @eq R (FtoRradix (Fminus radix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
unfold FtoRradix, FtoR, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (nNormMin radix precision) (Zpower_nat radix (Z.abs_nat (Z.sub (Z.succ (Fexp x)) (Z.min (Z.succ (Fexp x)) (Fexp x)))))) (Z.mul (Z.opp (Fnum x)) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Z.succ (Fexp x)) (Fexp x)))))))) (powerRZ (IZR radix) (Z.min (Z.succ (Fexp x)) (Fexp x)))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Fexp x))) *)
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
repeat rewrite Zmin_le2; auto with zarith.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (nNormMin radix precision) (Zpower_nat radix (Z.abs_nat (Z.sub (Z.succ (Fexp x)) (Fexp x))))) (Z.mul (Z.opp (Fnum x)) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Fexp x))))))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Fexp x))) *)
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
rewrite <- Zminus_succ_l; repeat rewrite <- Zminus_diag_reverse.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (Z.opp (pPred (vNum b))) (Zpower_nat radix (Z.abs_nat Z0))) (Z.mul (Z.opp (Fnum x)) (Zpower_nat radix (Z.abs_nat (Z.succ Z0)))))) (powerRZ (IZR radix) (Z.pred (Fexp x)))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.pred (Fexp x)))) *)
rewrite absolu_Zs; auto with zarith; simpl in |- *.
rewrite H'1; unfold pPred in |- *; rewrite pGivesBound;
 unfold nNormMin in |- *.
replace (Zpower_nat radix (pred precision) * (radix * 1))%Z with
(* Goal: @eq R (Rmult (Rplus (Ropp (Rplus (IZR (Zpower_nat radix precision)) (IZR (Zneg xH)))) (IZR (Zpower_nat radix precision))) (powerRZ (IZR radix) (Z.add (Fexp x) (Zneg xH)))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.add (Fexp x) (Zneg xH)))) *)
(* Goal: @eq Z (Zpower_nat radix precision) (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) radix) *)
 (Zpower_nat radix precision). f_equal. unfold Zpred.
(* Goal: @eq R (IZR (Z.add (Zpower_nat radix precision) (Z.mul (Z.opp (Z.add (Zpower_nat radix precision) (Zneg xH))) (Zpos xH)))) (IZR (Zpos xH)) *)
(* Goal: @eq Z (Zpower_nat radix precision) (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) (Z.mul radix (Zpos xH))) *)
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
rewrite Z.opp_add_distr. rewrite Z.mul_1_r. rewrite Z.add_assoc. now rewrite Z.add_opp_diag_r.
(*rewrite plus_IZR; rewrite Rmult_IZR; simpl in |- *.
unfold Zpred in |- *; unfold Zminus in |- *; simpl in |- *.
(* Goal: @eq Z (Z.mul (nNormMin radix precision) (Z.mul radix (Zpos xH))) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
repeat ring_simplify. ring.*) rewrite Z.mul_1_r.
(* Goal: @eq Z (Zpower_nat radix precision) (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) radix) *)
pattern precision at 1 in |- *; replace precision with (pred precision + 1).
(* Goal: @eq Z (Zpower_nat radix (Init.Nat.add (Init.Nat.pred precision) (S O))) (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) radix) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.pred precision) (S O)) precision *)
rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1; auto.
generalize precisionNotZero; case precision; simpl in |- *;
 auto with zarith arith.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FSuccSimpl4; auto.
(* Goal: @eq R (FtoRradix (Fminus radix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
unfold FtoRradix, FtoR, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (Z.succ (Fnum x)) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp x)))))) (Z.mul (Z.opp (Fnum x)) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp x)))))))) (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp x)))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Fexp x))) *)
repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (Z.succ (Fnum x)) (Zpos xH)) (Z.mul (Z.opp (Fnum x)) (Zpos xH)))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Fexp x))) *)
repeat rewrite Zmult_1_r.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.succ (Fnum x)) (Z.opp (Fnum x)))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Fexp x))) *)
replace (Zsucc (Fnum x) + - Fnum x)%Z with (Z_of_nat 1).
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
simpl in |- *; auto.
(* Goal: @eq Z (Z.of_nat (S O)) (Z.add (Z.succ (Fnum x)) (Z.opp (Fnum x))) *)
simpl in |- *; unfold Zsucc in |- *; ring.
Qed.
 
Theorem FSuccDiff2 :
 forall x : float,
 Fnum x = (- nNormMin radix precision)%Z ->
 Fexp x = (- dExp b)%Z -> Fminus radix (FSucc x) x = Float 1%nat (Fexp x) :>R.
(* Goal: forall (x : float) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))), @eq R (FtoRradix (Fminus radix (FSucc x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
intros x H' H'0; replace x with (Float (Fnum x) (Fexp x)).
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc (Float (Fnum x) (Fexp x))) (Float (Fnum x) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp (Float (Fnum x) (Fexp x))))) *)
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
rewrite H'; rewrite H'0; rewrite FSuccSimpl3; auto.
(* Goal: @eq R (FtoRradix (Fminus radix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
unfold FtoRradix, FtoR, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto.
repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse;
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (Z.succ (Fnum x)) (Zpos xH)) (Z.mul (Z.opp (Fnum x)) (Zpos xH)))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Fexp x))) *)
simpl in |- *; repeat rewrite Zmult_1_r.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite Zplus_succ_l; rewrite Zplus_opp_r; simpl in |- *; auto.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case x; simpl in |- *; auto.
Qed.
 
Theorem FSuccDiff3 :
 forall x : float,
 Fnum x = (- nNormMin radix precision)%Z ->
 Fexp x <> (- dExp b)%Z ->
 Fminus radix (FSucc x) x = Float 1%nat (Zpred (Fexp x)) :>R.
(* Goal: forall (x : float) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))), @eq R (FtoRradix (Fminus radix (FSucc x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
intros x H' H'1; rewrite FSuccSimpl2; auto.
(* Goal: @eq R (FtoRradix (Fminus radix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
unfold FtoRradix, FtoR, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (Z.opp (pPred (vNum b))) (Zpower_nat radix (Z.abs_nat (Z.sub (Z.pred (Fexp x)) (Z.min (Z.pred (Fexp x)) (Fexp x)))))) (Z.mul (Z.opp (Fnum x)) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Z.pred (Fexp x)) (Fexp x)))))))) (powerRZ (IZR radix) (Z.min (Z.pred (Fexp x)) (Fexp x)))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.pred (Fexp x)))) *)
repeat rewrite Zmin_le1; auto with zarith.
rewrite <- Zminus_diag_reverse; rewrite <- Zminus_n_predm;
 repeat rewrite <- Zminus_diag_reverse.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (Z.opp (pPred (vNum b))) (Zpower_nat radix (Z.abs_nat Z0))) (Z.mul (Z.opp (Fnum x)) (Zpower_nat radix (Z.abs_nat (Z.succ Z0)))))) (powerRZ (IZR radix) (Z.pred (Fexp x)))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.pred (Fexp x)))) *)
rewrite absolu_Zs; auto with zarith; simpl in |- *.
rewrite H'; unfold pPred in |- *; rewrite pGivesBound;
 unfold nNormMin in |- *.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (Z.succ (Fnum x)) (Zpos xH)) (Z.mul (Z.opp (Fnum x)) (Zpos xH)))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Fexp x))) *)
rewrite Zopp_involutive; repeat rewrite Zmult_1_r.
replace (Zpower_nat radix (pred precision) * radix)%Z with
 (Zpower_nat radix precision).
unfold Zpred in |- *; simpl in |- *;
(* Goal: @eq R (Rmult (Rplus (Ropp (Rplus (IZR (Zpower_nat radix precision)) (IZR (Zneg xH)))) (IZR (Zpower_nat radix precision))) (powerRZ (IZR radix) (Z.add (Fexp x) (Zneg xH)))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.add (Fexp x) (Zneg xH)))) *)
(* Goal: @eq Z (Zpower_nat radix precision) (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) radix) *)
 repeat rewrite plus_IZR || rewrite Ropp_Ropp_IZR. f_equal.
(* Goal: @eq R (Rplus (Ropp (Rplus (IZR (Zpower_nat radix precision)) (IZR (Zneg xH)))) (IZR (Zpower_nat radix precision))) (IZR (Zpos xH)) *)
(* Goal: @eq Z (Zpower_nat radix precision) (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) radix) *)
simpl in |- *; ring.
(* Goal: @eq Z (Zpower_nat radix precision) (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) radix) *)
pattern precision at 1 in |- *; replace precision with (pred precision + 1).
(* Goal: @eq Z (Zpower_nat radix (Init.Nat.add (Init.Nat.pred precision) (S O))) (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) radix) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.pred precision) (S O)) precision *)
rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1; auto.
generalize precisionNotZero; case precision; simpl in |- *;
 auto with zarith arith.
Qed.
 
Theorem ZltNormMinVnum : (nNormMin radix precision < Zpos (vNum b))%Z.
(* Goal: Z.lt (nNormMin radix precision) (Zpos (vNum b)) *)
unfold nNormMin in |- *; rewrite pGivesBound; auto with zarith.
Qed.
Hint Resolve ZltNormMinVnum: float.
 
Theorem FSuccNormPos :
 forall a : float,
 (0 <= a)%R -> Fnormal radix b a -> Fnormal radix b (FSucc a).
intros a H' H'0; unfold FSucc in |- *.
cut (Fbounded b a);
 [ intros B0 | apply FnormalBounded with (1 := H'0); auto ].
generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b)));
 case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
intros H'3; repeat split; simpl in |- *; auto.
(* Goal: Z.lt (Z.abs (nNormMin radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
rewrite Zabs_eq; auto with float zarith.
(* Goal: Z.le Z0 (nNormMin radix precision) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
unfold nNormMin in |- *; auto with zarith.
apply Zle_trans with (m := Fexp a); auto with float zarith arith.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
pattern precision at 1 in |- *; replace precision with (1 + pred precision).
rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1; unfold nNormMin in |- *;
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
generalize precisionNotZero; case precision; auto with zarith.
apply Zle_mult_gen; simpl in |- *; auto with zarith.
apply Zle_trans with 1%Z; auto with zarith.
(* Goal: Z.le Z0 (nNormMin radix precision) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
unfold nNormMin in |- *; auto with zarith.
intros H'3;
 generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum a) (- nNormMin radix precision)).
intros H'4; absurd (0 <= Fnum a)%Z; auto.
2: apply LeR0Fnum with (radix := radix); auto with zarith.
rewrite H'4; auto.
apply Zlt_not_le.
(* Goal: Z.le Z0 (nNormMin radix precision) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
replace 0%Z with (- 0%nat)%Z; unfold nNormMin in |- *; auto with zarith.
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Fnormal radix b (Float (Z.succ (Fnum a)) (Fexp a)) *)
intros H'4; repeat split; simpl in |- *; auto with float zarith arith.
apply Zle_lt_trans with (Zsucc (Zabs (Fnum a))); auto with float zarith.
case (Zlt_next (Zabs (Fnum a)) (Zpos (vNum b)));
 auto with float zarith arith.
intros H1; Contradict H'3.
unfold pPred in |- *; rewrite H1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.le Z0 (Fnum x) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
apply Zle_trans with (Zabs (radix * Fnum a)); auto with float zarith.
case H'0; auto.
repeat rewrite Zabs_Zmult.
cut (0 <= Fnum a)%Z; [ intros Z1 | apply LeR0Fnum with (radix := radix) ];
 auto.
rewrite (Zabs_eq (Fnum a)); auto.
rewrite (Zabs_eq (Zsucc (Fnum a))); auto with zarith.
Qed.
 
Theorem FSuccSubnormNotNearNormMin :
 forall a : float,
 Fsubnormal radix b a ->
 Fnum a <> Zpred (nNormMin radix precision) -> Fsubnormal radix b (FSucc a).
(* Goal: forall (a : float) (_ : Fsubnormal radix b a) (_ : @eq Z (Fnum a) (Z.pred (nNormMin radix precision))), Fnormal radix b (FSucc a) *)
intros a H' H'0.
cut (Fbounded b a);
 [ intros B0 | apply FsubnormalFbounded with (1 := H'); auto ].
(* Goal: Fnormal radix b (FSucc a) *)
unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b)));
 case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto.
intros H'2; absurd (Fdigit radix a < precision); auto with float.
2: apply FsubnormalDigit with (b := b); auto.
unfold Fdigit in |- *; rewrite H'2.
unfold pPred in |- *;
 rewrite
  (digitPredVNumiSPrecision radix) with (b := b) (precision := precision);
 auto with arith.
intros H'3;
 generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum a) (- nNormMin radix precision)).
intros H'2; absurd (Fdigit radix a < precision); auto with float.
unfold Fdigit in |- *; rewrite H'2.
replace (digit radix (- nNormMin radix precision)) with
 (digit radix (nNormMin radix precision)).
rewrite digitnNormMin; auto with arith.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case (nNormMin radix precision); simpl in |- *; auto.
apply FsubnormalDigit with (b := b); auto.
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Fnormal radix b (Float (Z.succ (Fnum a)) (Fexp a)) *)
intros H'4; repeat split; simpl in |- *; auto with float zarith arith.
apply Zle_lt_trans with (m := Zsucc (Zabs (Fnum a)));
 auto with float zarith arith.
apply Zlt_le_trans with (m := Zsucc (nNormMin radix precision));
 auto with float zarith arith.
apply Zsucc_lt_compat; apply pSubnormal_absolu_min with (3 := pGivesBound);
 auto with float zarith arith.
case H'; intros H1 (H2, H3); auto with float.
rewrite Zabs_Zmult.
rewrite (Zabs_eq radix); auto with zarith.
apply Zlt_le_trans with (m := (radix * nNormMin radix precision)%Z);
 auto with float zarith arith.
apply Zmult_gt_0_lt_compat_l; try apply Zlt_gt; auto with zarith.
(* Goal: Z.lt (Z.abs (Z.succ (Fnum f))) (Zpos (vNum b)) *)
apply Zlt_Zabs_Zpred; auto with float zarith arith.
apply pSubnormal_absolu_min with (3 := pGivesBound); auto.
pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix);
 unfold nNormMin in |- *; rewrite <- Zpower_nat_is_exp.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Zpower_nat radix (Init.Nat.add (S O) (Init.Nat.pred precision)))) *)
rewrite pGivesBound.
(* Goal: Z.le (Zpower_nat radix precision) (Z.abs (Zpower_nat radix (Init.Nat.add (S O) (Init.Nat.pred precision)))) *)
generalize precisionNotZero; case precision; simpl in |- *; auto with zarith.
Qed.
 
Theorem FSuccSubnormNearNormMin :
 forall a : float,
 Fsubnormal radix b a ->
 Fnum a = Zpred (nNormMin radix precision) -> Fnormal radix b (FSucc a).
(* Goal: forall (a : float) (_ : Fsubnormal radix b a) (_ : @eq Z (Fnum a) (Z.pred (nNormMin radix precision))), Fnormal radix b (FSucc a) *)
intros a H' H'0.
(* Goal: Fnormal radix b (FSucc a) *)
cut (Fbounded b a); [ intros Fb0 | apply FsubnormalFbounded with (1 := H') ].
(* Goal: Fnormal radix b (FSucc a) *)
unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b)));
 case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto.
intros H'1; absurd (nNormMin radix precision < Zpos (vNum b))%Z;
 auto with float.
(* Goal: not (Z.lt (Z.opp (nNormMin radix precision)) (Fnum y)) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Zle_not_lt.
apply Zle_n_Zpred; unfold pPred in H'1; rewrite <- H'1; rewrite H'0;
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
intros H'3;
 generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum a) (- nNormMin radix precision)).
intros H'1;
 absurd (- nNormMin radix precision < Zpred (nNormMin radix precision))%Z.
(* Goal: not (Z.lt (Z.opp (nNormMin radix precision)) (Z.pred (nNormMin radix precision))) *)
(* Goal: Z.lt (Z.opp (nNormMin radix precision)) (Z.pred (nNormMin radix precision)) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Fnormal radix b (Float (Z.succ (Fnum a)) (Fexp a)) *)
rewrite <- H'1; rewrite <- H'0; auto with zarith.
unfold nNormMin in |- *; apply Zlt_le_trans with (m := (- (0))%Z);
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Fnormal radix b (Float (Z.succ (Fnum a)) (Fexp a)) *)
intros H'4; repeat split; simpl in |- *; auto with float zarith arith.
(* Goal: @eq Z (Z.mul (nNormMin radix precision) radix) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite H'0.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix (Z.succ (Z.pred (nNormMin radix precision))))) *)
rewrite <- Zsucc_pred.
(* Goal: Z.lt (Z.abs (nNormMin radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
rewrite Zabs_eq; auto with float zarith.
(* Goal: Z.le Z0 (nNormMin radix precision) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
unfold nNormMin in |- *; auto with zarith.
(* Goal: @eq Z (Z.mul (nNormMin radix precision) radix) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite H'0.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix (Z.succ (Z.pred (nNormMin radix precision))))) *)
rewrite <- Zsucc_pred.
pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix);
 unfold nNormMin in |- *; rewrite <- Zpower_nat_is_exp.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Zpower_nat radix (Init.Nat.add (S O) (Init.Nat.pred precision)))) *)
rewrite pGivesBound.
(* Goal: Z.le (Zpower_nat radix precision) (Z.abs (Zpower_nat radix (Init.Nat.add (S O) (Init.Nat.pred precision)))) *)
generalize precisionNotZero; case precision; simpl in |- *; auto with zarith.
Qed.
 
Theorem FBoundedSuc : forall f : float, Fbounded b f -> Fbounded b (FSucc f).
(* Goal: Fnormal radix b (FSucc a) *)
intros f H'; unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum f) (pPred (vNum b)));
 case (Z_eq_bool (Fnum f) (pPred (vNum b))); intros H'1.
(* Goal: Fbounded b (Float (nNormMin radix precision) (Z.succ (Fexp f))) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
repeat split; simpl in |- *; auto with zarith arith.
(* Goal: Z.lt (Z.abs (nNormMin radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
rewrite Zabs_eq; auto with float zarith.
(* Goal: Z.le Z0 (nNormMin radix precision) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
unfold nNormMin in |- *; auto with zarith.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
apply Zle_trans with (Fexp f); auto with float zarith.
generalize (Z_eq_bool_correct (Fnum f) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum f) (- nNormMin radix precision)); 
 intros H'2.
generalize (Z_eq_bool_correct (Fexp f) (- dExp b));
 case (Z_eq_bool (Fexp f) (- dExp b)); intros H'3.
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
repeat split; simpl in |- *; auto with float zarith arith.
(* Goal: Z.lt (Z.abs (Z.succ (Fnum f))) (Zpos (vNum b)) *)
apply Zlt_Zabs_Zpred; auto with float zarith arith.
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
repeat split; simpl in |- *; auto with float zarith arith.
(* Goal: Z.lt (Z.abs (Z.opp (pPred (vNum b)))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.pred (Fexp f)) *)
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
rewrite Zabs_Zopp.
(* Goal: Z.lt (Z.abs (pPred (vNum b))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.pred (Fexp f)) *)
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
rewrite Zabs_eq; unfold pPred in |- *; auto with zarith.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.pred (Fexp f)) *)
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
case (Zle_next (- dExp b) (Fexp f)); auto with float zarith arith.
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
repeat split; simpl in |- *; auto with float zarith arith.
(* Goal: Z.lt (Z.abs (Z.succ (Fnum f))) (Zpos (vNum b)) *)
apply Zlt_Zabs_Zpred; auto with float zarith arith.
Qed.
 
Theorem FSuccSubnormal :
 forall a : float, Fsubnormal radix b a -> Fcanonic radix b (FSucc a).
(* Goal: forall (a : float) (_ : Fcanonic radix b a), Fcanonic radix b (FSucc a) *)
intros a H'.
generalize (Z_eq_bool_correct (Fnum a) (Zpred (nNormMin radix precision)));
 case (Z_eq_bool (Fnum a) (Zpred (nNormMin radix precision))); 
 intros H'1.
(* Goal: Fcanonic radix b (FSucc a) *)
(* Goal: Fcanonic radix b (FSucc a) *)
left; apply FSuccSubnormNearNormMin; auto.
(* Goal: Fcanonic radix b (FSucc a) *)
right; apply FSuccSubnormNotNearNormMin; auto.
Qed.
 
Theorem FSuccPosNotMax :
 forall a : float,
 (0 <= a)%R -> Fcanonic radix b a -> Fcanonic radix b (FSucc a).
(* Goal: forall (a : float) (_ : Rle (IZR Z0) (FtoRradix a)) (_ : Fcanonic radix b a), Fcanonic radix b (FSucc a) *)
intros a H' H'0; case H'0; intros H'2.
(* Goal: Fcanonic radix b (FSucc a) *)
(* Goal: Fcanonic radix b (FSucc a) *)
left; apply FSuccNormPos; auto.
(* Goal: Fcanonic radix b (FSucc a) *)
apply FSuccSubnormal; auto.
Qed.
 
Theorem FSuccNormNegNotNormMin :
 forall a : float,
 (a <= 0)%R ->
 Fnormal radix b a ->
 a <> Float (- nNormMin radix precision) (- dExp b) ->
 Fnormal radix b (FSucc a).
intros a H' H'0 H'1; cut (Fbounded b a);
 [ intros Fb0 | apply FnormalBounded with (1 := H'0) ].
cut (Fnum a <= 0)%Z; [ intros Z0 | apply R0LeFnum with (radix := radix) ];
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
case (Zle_lt_or_eq _ _ Z0); intros Z1.
2: absurd (is_Fzero a); auto with float.
2: apply FnormalNotZero with (1 := H'0); auto.
(* Goal: Fnormal radix b (FSucc a) *)
unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b)));
 case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto.
intros H'2; absurd (0 < Fnum a)%Z; auto with zarith arith.
rewrite H'2; unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *;
 apply (vNumbMoreThanOne radix) with (precision := precision);
 auto with zarith arith.
intros H'3;
 generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum a) (- nNormMin radix precision)); 
 auto.
intros H'2; generalize (Z_eq_bool_correct (Fexp a) (- dExp b));
 case (Z_eq_bool (Fexp a) (- dExp b)).
intros H'4; Contradict H'1; auto.
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply floatEq; auto.
intros H'4; repeat split; simpl in |- *; auto with zarith.
(* Goal: Z.lt (Z.abs (Z.opp (pPred (vNum b)))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.pred (Fexp f)) *)
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
rewrite Zabs_Zopp.
unfold pPred in |- *; rewrite Zabs_eq; auto with zarith.
case (Zle_next (- dExp b) (Fexp a)); auto with float zarith.
(* Goal: Z.lt (Z.abs (Z.opp (pPred (vNum b)))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.pred (Fexp f)) *)
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
rewrite <- Zopp_mult_distr_r; rewrite Zabs_Zopp.
rewrite Zabs_Zmult.
(* Goal: Z.lt (Z.abs (nNormMin radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.succ (Fexp f)) *)
(* Goal: Fbounded b (if Z_eq_bool (Fnum f) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp f) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum f)) (Fexp f) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp f)) else Float (Z.succ (Fnum f)) (Fexp f)) *)
repeat rewrite Zabs_eq; auto with float zarith.
pattern (Zpos (vNum b)) at 1 in |- *;
 rewrite (PosNormMin radix) with (precision := precision); 
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
apply Zle_Zmult_comp_l; auto with zarith.
unfold pPred in |- *; apply Zle_Zpred; auto with float zarith.
unfold pPred in |- *; apply Zle_Zpred; auto with float zarith.
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
intros H'2; repeat split; simpl in |- *; auto with float zarith arith.
apply Zlt_trans with (Zabs (Fnum a)); auto with float zarith.
repeat rewrite Zabs_eq_opp; auto with float zarith.
rewrite Zabs_Zmult.
rewrite (Zabs_eq radix);
 [ idtac | apply Zle_trans with 1%Z; auto with zarith ].
repeat rewrite Zabs_eq_opp; auto with float zarith.
pattern (Zpos (vNum b)) at 1 in |- *;
 rewrite (PosNormMin radix) with (precision := precision); 
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
apply Zle_Zmult_comp_l; auto with zarith.
replace (- Zsucc (Fnum a))%Z with (Zpred (- Fnum a)).
auto with float zarith.
unfold pPred in |- *; apply Zle_Zpred.
case (Zle_lt_or_eq (nNormMin radix precision) (- Fnum a)); auto.
rewrite <- Zabs_eq_opp; auto with float zarith.
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum y)) *)
(* Goal: Z.le Z0 (Fnum y) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: Rle (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp x)))) (FtoRradix y) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply pNormal_absolu_min with (b := b); auto.
intros H'4; Contradict H'2; rewrite H'4; ring.
apply Zpred_Zopp_Zs; auto.
Qed.
 
Theorem FSuccNormNegNormMin :
 Fsubnormal radix b (FSucc (Float (- nNormMin radix precision) (- dExp b))).
(* Goal: @eq float (FSucc (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))) *)
unfold FSucc in |- *; simpl in |- *.
generalize (Z_eq_bool_correct (- nNormMin radix precision) (pPred (vNum b)));
 case (Z_eq_bool (- nNormMin radix precision) (pPred (vNum b))); 
 intros H'; auto.
absurd (0%nat < pPred (vNum b))%Z; auto.
rewrite <- H'; auto with float zarith.
replace (Z_of_nat 0) with (- (0))%Z; [ idtac | simpl in |- *; auto ].
apply Zle_not_lt; apply Zle_Zopp; auto with float zarith.
apply Zlt_le_weak; auto with float zarith.
apply nNormPos; auto with float zarith.
unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *;
 auto with float zarith.
apply (vNumbMoreThanOne radix) with (precision := precision);
 auto with float zarith.
generalize
 (Z_eq_bool_correct (- nNormMin radix precision) (- nNormMin radix precision));
 case (Z_eq_bool (- nNormMin radix precision) (- nNormMin radix precision));
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
 intros H'0.
2: Contradict H'0; auto.
generalize (Z_eq_bool_correct (- dExp b) (- dExp b));
 case (Z_eq_bool (- dExp b) (- dExp b)); intros H'1.
2: Contradict H'1; auto.
repeat split; simpl in |- *; auto with zarith.
apply Zle_lt_trans with (m := nNormMin radix precision);
 auto with float zarith.
rewrite <- Zopp_Zpred_Zs; rewrite Zabs_Zopp; rewrite Zabs_eq;
 auto with float zarith.
apply Zle_Zpred; simpl in |- *; auto with float zarith.
apply nNormPos; auto with float zarith.
rewrite Zabs_Zmult; rewrite (Zabs_eq radix); auto with zarith.
rewrite (PosNormMin radix) with (precision := precision); auto with zarith.
apply Zmult_gt_0_lt_compat_l; auto with float zarith.
(* Goal: Z.lt (Z.abs (Z.opp (pPred (vNum b)))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.pred (Fexp f)) *)
(* Goal: Fbounded b (Float (Z.succ (Fnum f)) (Fexp f)) *)
rewrite <- Zopp_Zpred_Zs; rewrite Zabs_Zopp.
rewrite Zabs_eq; auto with zarith.
apply Zle_Zpred; simpl in |- *; auto with float zarith.
apply nNormPos; auto with float zarith.
Qed.
 
Theorem FSuccNegCanonic :
 forall a : float,
 (a <= 0)%R -> Fcanonic radix b a -> Fcanonic radix b (FSucc a).
(* Goal: forall (a : float) (_ : Rle (FtoRradix a) (IZR Z0)) (_ : Fcanonic radix b a), Fcanonic radix b (FSucc a) *)
intros a H' H'0; case H'0; intros H'1.
(* Goal: Fcanonic radix b (FSucc a) *)
(* Goal: Fcanonic radix b (FSucc a) *)
case (floatDec a (Float (- nNormMin radix precision) (- dExp b))); intros H'2.
(* Goal: Fcanonic radix b (FSucc a) *)
(* Goal: Fcanonic radix b (FSucc a) *)
(* Goal: Fcanonic radix b (FSucc a) *)
rewrite H'2; right; apply FSuccNormNegNormMin; auto.
(* Goal: Fcanonic radix b (FSucc a) *)
(* Goal: Fcanonic radix b (FSucc a) *)
left; apply FSuccNormNegNotNormMin; auto.
(* Goal: Fcanonic radix b (FSucc a) *)
apply FSuccSubnormal; auto.
Qed.
 
Theorem FSuccCanonic :
 forall a : float, Fcanonic radix b a -> Fcanonic radix b (FSucc a).
(* Goal: forall (a : float) (_ : Fcanonic radix b a), Fcanonic radix b (FSucc a) *)
intros a H'.
(* Goal: Fcanonic radix b (FSucc a) *)
case (Rle_or_lt 0 a); intros H'3.
(* Goal: Fcanonic radix b (FSucc a) *)
(* Goal: Fcanonic radix b (FSucc a) *)
apply FSuccPosNotMax; auto.
(* Goal: Fcanonic radix b (FSucc a) *)
apply FSuccNegCanonic; auto with real.
Qed.
 
Theorem FSuccLt : forall a : float, (a < FSucc a)%R.
(* Goal: Fnormal radix b (FSucc a) *)
intros a; unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b)));
 case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto.
(* Goal: forall _ : @eq Z (Fnum a) (pPred (vNum b)), Rlt (FtoRradix a) (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp a)))) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rlt (FtoRradix a) (FtoRradix (if Z_eq_bool (Fnum a) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp a) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum a)) (Fexp a) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp a)) else Float (Z.succ (Fnum a)) (Fexp a))) *)
intros H'; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite H'.
unfold pPred in |- *;
 rewrite (PosNormMin radix) with (precision := precision); 
 auto with zarith; unfold nNormMin in |- *.
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (powerRZ (IZR radix) (Z.succ (Z.pred (Fexp a))))) (Rmult (IZR (Z.opp (pPred (vNum b)))) (powerRZ (IZR radix) (Z.pred (Fexp a)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
rewrite powerRZ_Zs; auto with real zarith.
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (Rmult (IZR radix) (powerRZ (IZR radix) (Z.pred (Fexp a))))) (Rmult (IZR (Z.opp (pPred (vNum b)))) (powerRZ (IZR radix) (Z.pred (Fexp a)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
repeat rewrite <- Rmult_assoc.
(* Goal: Rlt (Rmult (IZR (Z.pred (Z.mul radix (Zpower_nat radix (Init.Nat.pred precision))))) (powerRZ (IZR radix) (Fexp a))) (Rmult (Rmult (IZR (Zpower_nat radix (Init.Nat.pred precision))) (IZR radix)) (powerRZ (IZR radix) (Fexp a))) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rlt (FtoRradix a) (FtoRradix (if Z_eq_bool (Fnum a) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp a) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum a)) (Fexp a) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp a)) else Float (Z.succ (Fnum a)) (Fexp a))) *)
apply Rlt_monotony_exp; auto with zarith.
(* Goal: Z.lt (pPred (vNum b)) (Z.mul (nNormMin radix precision) radix) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
rewrite Zmult_comm.
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (IZR radix)) (IZR (Z.opp (pPred (vNum b)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
rewrite <- Rmult_IZR.
(* Goal: Rlt (IZR (Z.mul (Z.opp (nNormMin radix precision)) radix)) (IZR (Z.opp (pPred (vNum b)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
apply Rlt_IZR; auto with zarith.
intros H';
 generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum a) (- nNormMin radix precision)).
intros H'0; generalize (Z_eq_bool_correct (Fexp a) (- dExp b));
 case (Z_eq_bool (Fexp a) (- dExp b)).
(* Goal: forall _ : @eq Z (Fexp a) (Z.opp (Z.of_N (dExp b))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
(* Goal: forall _ : not (@eq Z (Fexp a) (Z.opp (Z.of_N (dExp b)))), Rlt (FtoRradix a) (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp a)))) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
intros H'1; unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: Rlt (Rmult (Rmult (IZR (Z.opp (nNormMin radix precision))) (IZR radix)) (powerRZ (IZR radix) (Z.pred (Fexp a)))) (Rmult (IZR (Z.opp (pPred (vNum b)))) (powerRZ (IZR radix) (Z.pred (Fexp a)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
apply Rlt_monotony_exp; auto with real zarith.
(* Goal: @eq Z (Z.mul (nNormMin radix precision) radix) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
intros H'1; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite H'0.
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (powerRZ (IZR radix) (Fexp a))) (Rmult (IZR (Z.opp (pPred (vNum b)))) (powerRZ (IZR radix) (Z.pred (Fexp a)))) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
pattern (Fexp a) at 1 in |- *; replace (Fexp a) with (Zsucc (Zpred (Fexp a))).
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (powerRZ (IZR radix) (Z.succ (Z.pred (Fexp a))))) (Rmult (IZR (Z.opp (pPred (vNum b)))) (powerRZ (IZR radix) (Z.pred (Fexp a)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
rewrite powerRZ_Zs; auto with real zarith.
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (Rmult (IZR radix) (powerRZ (IZR radix) (Z.pred (Fexp a))))) (Rmult (IZR (Z.opp (pPred (vNum b)))) (powerRZ (IZR radix) (Z.pred (Fexp a)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
repeat rewrite <- Rmult_assoc.
(* Goal: Rlt (Rmult (Rmult (IZR (Z.opp (nNormMin radix precision))) (IZR radix)) (powerRZ (IZR radix) (Z.pred (Fexp a)))) (Rmult (IZR (Z.opp (pPred (vNum b)))) (powerRZ (IZR radix) (Z.pred (Fexp a)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
apply Rlt_monotony_exp; auto with real zarith.
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (IZR radix)) (IZR (Z.opp (pPred (vNum b)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
rewrite <- Rmult_IZR.
(* Goal: Rlt (IZR (Z.mul (Z.opp (nNormMin radix precision)) radix)) (IZR (Z.opp (pPred (vNum b)))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
apply Rlt_IZR; auto with zarith.
(* Goal: Z.lt (Z.mul (Z.opp (nNormMin radix precision)) radix) (Z.opp (pPred (vNum b))) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
rewrite <- Zopp_mult_distr_l.
(* Goal: Z.lt (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_nat O)) *)
(* Goal: Z.le Z0 (Fnum x) *)
apply Zlt_Zopp.
(* Goal: Z.lt (pPred (vNum b)) (Z.mul (nNormMin radix precision) radix) *)
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
rewrite Zmult_comm.
unfold pPred in |- *;
 rewrite (PosNormMin radix) with (precision := precision); 
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
(* Goal: @eq Z (Z.succ (Z.pred (Fexp a))) (Fexp a) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (Z.opp (nNormMin radix precision))), Rlt (FtoRradix a) (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) *)
apply sym_equal; apply Zsucc_pred.
intros H'1; unfold FtoRradix, FtoR in |- *; simpl in |- *;
 auto with real zarith.
Qed.
 
Theorem FSuccPropPos :
 forall x y : float,
 (0 <= x)%R ->
 Fcanonic radix b x -> Fcanonic radix b y -> (x < y)%R -> (FSucc x <= y)%R.
(* Goal: forall (x y : float) (_ : Rlt (FtoRradix x) (IZR Z0)) (_ : Fcanonic radix b x) (_ : Fcanonic radix b y) (_ : Rlt (FtoRradix x) (FtoRradix y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
intros x y H' H'0 H'1 H'2.
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
cut (Fbounded b x); [ intros Fb0 | apply FcanonicBound with (1 := H'0) ].
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
cut (Fbounded b y); [ intros Fb1 | apply FcanonicBound with (1 := H'1) ].
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
case FcanonicLtPos with (p := x) (q := y) (3 := pGivesBound); auto.
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
case (Z_eq_dec (Fnum x) (pPred (vNum b))); intros H'4.
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite FSuccSimpl1; auto.
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp x)))) (FtoRradix y) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
intros H'5; case (Zlt_next _ _ H'5); intros H'6.
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
replace y with (Float (Fnum y) (Fexp y)).
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite H'6.
generalize Fle_Zle; unfold Fle, FtoRradix in |- *; intros H'7; apply H'7;
 clear H'7; auto with arith.
rewrite <- (Zabs_eq (Fnum y)); auto with float zarith.
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum y)) *)
(* Goal: Z.le Z0 (Fnum y) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: Rle (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp x)))) (FtoRradix y) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply pNormal_absolu_min with (b := b); auto.
(* Goal: Fnormal radix b y *)
(* Goal: Z.le Z0 (Fnum y) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: Rle (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp x)))) (FtoRradix y) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
case H'1; auto with float.
(* Goal: not (Z.lt (Z.opp (nNormMin radix precision)) (Fnum y)) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
intros H'7; Contradict H'5; apply Zle_not_lt.
(* Goal: Z.le (Fexp y) (Fexp x) *)
(* Goal: Z.le Z0 (Fnum y) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: Rle (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp x)))) (FtoRradix y) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
replace (Fexp y) with (- dExp b)%Z; auto with float.
(* Goal: @eq Z (Z.opp (Z.of_N (dExp b))) (Fexp y) *)
(* Goal: Z.le Z0 (Fnum y) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: Rle (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp x)))) (FtoRradix y) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
case H'7; intros H'8 (H'9, H'10); auto.
(* Goal: Z.le Z0 (Fnum x) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (FSucc x) *)
(* Goal: Z.lt (Fexp (FSucc x)) (Fexp y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Rle_trans with (r2 := FtoR radix x); auto with real.
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case y; auto.
(* Goal: Rle (FtoR radix y) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Float (Z.succ (Fnum x)) (Fexp x))) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Rlt_le; auto.
unfold FtoRradix in |- *; apply FcanonicPosFexpRlt with (3 := pGivesBound);
 auto.
(* Goal: Rle (IZR Z0) (FtoR radix (Float (nNormMin radix precision) (Z.succ (Fexp x)))) *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply LeFnumZERO with (radix := radix); auto with zarith.
(* Goal: not (@eq Z (Fnum (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (Z.opp (nNormMin radix precision))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
simpl in |- *; auto with zarith.
(* Goal: Z.le Z0 (nNormMin radix precision) *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zlt_le_weak; apply nNormPos.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
auto with zarith.
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (FSucc x) *)
(* Goal: Z.lt (Fexp (FSucc x)) (Fexp y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Rle_trans with (r2 := FtoR radix x); auto with real.
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite <- FSuccSimpl1; auto.
(* Goal: Fcanonic radix b (FSucc x) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply FSuccCanonic; auto.
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
intros H'5; apply Rlt_le.
unfold FtoRradix in |- *; apply FcanonicPosFexpRlt with (3 := pGivesBound);
 auto.
(* Goal: Rle (IZR Z0) (FtoR radix (FSucc x)) *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (FSucc x) *)
(* Goal: Z.lt (Fexp (FSucc x)) (Fexp y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Rle_trans with (r2 := FtoR radix x); auto.
(* Goal: Rle (FtoR radix y) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Float (Z.succ (Fnum x)) (Fexp x))) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Rlt_le; auto.
(* Goal: Rlt (FtoR radix (Fnormalize radix b precision a)) (FtoR radix (FSucc (Fnormalize radix b precision a))) *)
apply FSuccLt; auto.
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (FSucc x) *)
(* Goal: Z.lt (Fexp (FSucc x)) (Fexp y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Rle_trans with (r2 := FtoR radix x); auto with real.
(* Goal: Fcanonic radix b (FSucc x) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply FSuccCanonic; auto.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FSuccSimpl4; auto.
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply sym_not_equal; apply Zlt_not_eq.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zlt_le_trans with (m := 0%Z); auto with zarith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
replace 0%Z with (- 0%nat)%Z; auto with zarith.
(* Goal: Z.lt (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_nat O)) *)
(* Goal: Z.le Z0 (Fnum x) *)
apply Zlt_Zopp.
(* Goal: Z.lt (Z.of_nat O) (nNormMin radix precision) *)
(* Goal: Z.le Z0 (Fnum x) *)
apply nNormPos; auto.
(* Goal: Z.le Z0 (Fnum x) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
intros H'4; elim H'4; intros H'5 H'6; clear H'4.
generalize (Z_eq_bool_correct (Fnum x) (Zpos (vNum b)));
 case (Z_eq_bool (Fnum x) (Zpos (vNum b))); 
 intros H'4.
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
Contradict H'6; auto.
(* Goal: not (Z.lt (Z.succ (Fnum x)) (Fnum y)) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
apply Zle_not_lt; apply Zlt_le_weak.
rewrite H'4; auto with float zarith.
rewrite <- (Zabs_eq (Fnum y)); auto with float zarith.
(* Goal: Z.le Z0 (Fnum x) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
apply Rle_trans with (FtoRradix x); auto with real.
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case (Zlt_next _ _ H'6); intros H'7.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FSuccSimpl4; auto.
rewrite <- H'7; rewrite H'5; unfold FtoRradix, FtoR in |- *; simpl in |- *;
 auto with real.
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Zlt_not_eq.
(* Goal: Z.lt (Fnum x) (pPred (vNum b)) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
unfold pPred in |- *; apply Zlt_succ_pred; rewrite <- H'7; auto with float.
rewrite <- (Zabs_eq (Fnum y)); auto with float zarith.
(* Goal: Z.le Z0 (Fnum x) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
apply Rle_trans with (FtoRradix x); auto with real.
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
apply Zlt_not_eq_rev.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zlt_le_trans with (m := 0%Z); auto with zarith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
replace 0%Z with (- 0%nat)%Z; auto with zarith.
(* Goal: Z.lt (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_nat O)) *)
(* Goal: Z.le Z0 (Fnum x) *)
apply Zlt_Zopp.
(* Goal: Z.lt (Z.of_nat O) (nNormMin radix precision) *)
(* Goal: Z.le Z0 (Fnum x) *)
apply nNormPos; auto.
(* Goal: Z.le Z0 (Fnum x) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FSuccSimpl4; auto.
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
replace y with (Float (Fnum y) (Fexp y)).
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
rewrite H'5.
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp y))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real float.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case y; simpl in |- *; auto.
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
Contradict H'7; auto.
(* Goal: not (Z.lt (Z.succ (Fnum x)) (Fnum y)) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
apply Zle_not_lt; apply Zlt_le_weak.
rewrite H'7; auto with float zarith.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix (Z.succ (Z.pred (nNormMin radix precision))))) *)
unfold pPred in |- *; rewrite <- Zsucc_pred.
rewrite <- (Zabs_eq (Fnum y)); auto with float zarith.
(* Goal: Z.le Z0 (Fnum x) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
apply Rle_trans with (FtoRradix x); auto with real.
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
apply Zlt_not_eq_rev.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zlt_le_trans with (m := 0%Z); auto with zarith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
replace 0%Z with (- 0%nat)%Z; auto with zarith.
(* Goal: Z.lt (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_nat O)) *)
(* Goal: Z.le Z0 (Fnum x) *)
apply Zlt_Zopp.
(* Goal: Z.lt (Z.of_nat O) (nNormMin radix precision) *)
(* Goal: Z.le Z0 (Fnum x) *)
apply nNormPos; auto.
(* Goal: Z.le Z0 (Fnum x) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
Qed.
 
Theorem R0RltRleSucc : forall x : float, (x < 0)%R -> (FSucc x <= 0)%R.
(* Goal: Fnormal radix b (FSucc a) *)
intros a H'; unfold FSucc in |- *.
generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b)));
 case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto.
(* Goal: forall _ : @eq Z (Fnum a) (pPred (vNum b)), Rle (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp a)))) (IZR Z0) *)
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (if Z_eq_bool (Fnum a) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp a) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum a)) (Fexp a) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp a)) else Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
intros H'0; absurd (Fnum a < 0)%Z; auto.
(* Goal: not (Z.lt (Fnum a) Z0) *)
(* Goal: Z.lt (Fnum a) Z0 *)
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (if Z_eq_bool (Fnum a) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp a) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum a)) (Fexp a) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp a)) else Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
rewrite H'0; auto with zarith arith.
(* Goal: not (Z.lt (pPred (vNum b)) Z0) *)
(* Goal: Z.lt (Fnum a) Z0 *)
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (if Z_eq_bool (Fnum a) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp a) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum a)) (Fexp a) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp a)) else Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
apply Zle_not_lt; unfold pPred in |- *; apply Zle_Zpred; auto with float.
apply Zlt_trans with 1%Z; auto with zarith;
 apply (vNumbMoreThanOne radix) with (precision := precision);
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply R0LtFnum with (radix := radix); auto with zarith.
generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum a) (- nNormMin radix precision)); 
 intros H'1.
generalize (Z_eq_bool_correct (Fexp a) (- dExp b));
 case (Z_eq_bool (Fexp a) (- dExp b)); intros H'2.
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
intros H'0.
(* Goal: not (@eq Z (Fnum (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (Z.opp (nNormMin radix precision))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply LeZEROFnum with (radix := radix); simpl in |- *; auto with zarith.
(* Goal: Z.le (Z.succ (Fnum a)) Z0 *)
apply Zlt_le_succ.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply R0LtFnum with (radix := radix); auto with zarith.
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
intros H'0.
(* Goal: not (@eq Z (Fnum (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (Z.opp (nNormMin radix precision))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply LeZEROFnum with (radix := radix); simpl in |- *; auto with zarith.
(* Goal: Z.le (Z.opp (pPred (vNum b))) Z0 *)
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
replace 0%Z with (- (0))%Z; [ apply Zle_Zopp | simpl in |- *; auto ].
unfold pPred in |- *; apply Zle_Zpred; apply Zlt_trans with 1%Z;
 auto with zarith;
 apply (vNumbMoreThanOne radix) with (precision := precision);
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
intros H'0.
(* Goal: not (@eq Z (Fnum (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (Z.opp (nNormMin radix precision))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply LeZEROFnum with (radix := radix); simpl in |- *; auto with zarith.
(* Goal: Z.le (Z.succ (Fnum a)) Z0 *)
apply Zlt_le_succ.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply R0LtFnum with (radix := radix); auto with zarith.
Qed.
 
Theorem FSuccPropNeg :
 forall x y : float,
 (x < 0)%R ->
 Fcanonic radix b x -> Fcanonic radix b y -> (x < y)%R -> (FSucc x <= y)%R.
(* Goal: forall (x y : float) (_ : Rlt (FtoRradix x) (IZR Z0)) (_ : Fcanonic radix b x) (_ : Fcanonic radix b y) (_ : Rlt (FtoRradix x) (FtoRradix y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
intros x y H' H'0 H'1 H'2.
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
cut (Fbounded b x); [ intros Fb0 | apply FcanonicBound with (1 := H'0) ].
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
cut (Fbounded b y); [ intros Fb1 | apply FcanonicBound with (1 := H'1) ].
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
case (Rle_or_lt 0 y); intros Rle0.
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Rle_trans with (r2 := 0%R); auto.
(* Goal: Rle (FtoR radix (FSucc x)) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply R0RltRleSucc; auto.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
cut (Fnum x <> pPred (vNum b)); [ intros N0 | idtac ]; auto with zarith.
generalize (Z_eq_bool_correct (Fnum x) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum x) (- nNormMin radix precision)); 
 intros H'4.
generalize (Z_eq_bool_correct (Fexp x) (- dExp b));
 case (Z_eq_bool (Fexp x) (- dExp b)); intros H'5.
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
replace x with (Float (Fnum x) (Fexp x)).
(* Goal: Rle (FtoRradix (FSucc (Float (Fnum x) (Fexp x)))) (FtoRradix y) *)
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite H'4; rewrite H'5; rewrite FSuccSimpl3; auto.
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case FcanonicLtNeg with (p := x) (q := y) (3 := pGivesBound); auto with real.
(* Goal: forall _ : Z.lt (Fexp y) (Fexp x), Rle (FtoRradix (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (FtoRradix y) *)
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
intros H'6; Contradict H'6; rewrite H'5; apply Zle_not_lt; auto with float.
intros H'6; elim H'6; intros H'7 H'8; clear H'6;
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
 replace y with (Float (Fnum y) (Fexp y)).
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
rewrite <- H'7; rewrite H'5.
generalize Fle_Zle; unfold Fle, FtoRradix in |- *; intros H'9; apply H'9;
 clear H'9; auto with arith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite <- H'4; auto with zarith.
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case y; auto.
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case x; auto.
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite FSuccSimpl2; auto.
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case FcanonicLtNeg with (p := x) (q := y) (3 := pGivesBound); auto with real.
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
intros H'6; replace y with (Float (Fnum y) (Fexp y)).
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case (Zlt_next _ _ H'6); intros H'7.
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite H'7.
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp y))))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite <- Zpred_succ.
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Fexp y))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Rle_monotone_exp; auto with zarith.
(* Goal: Rle (IZR (Z.opp (pPred (vNum b)))) (IZR (Fnum y)) *)
(* Goal: Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite <- (Zopp_involutive (Fnum y)); apply Rle_IZR; apply Zle_Zopp.
unfold pPred in |- *; apply Zle_Zpred; rewrite <- Zabs_eq_opp;
 auto with float zarith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zlt_le_weak; apply R0LtFnum with (radix := radix); auto with zarith.
(* Goal: Rle (FtoR radix y) (IZR Z0) *)
(* Goal: forall _ : Z.lt (Fexp y) (Fexp x), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Rlt_le; auto with real.
unfold FtoRradix in |- *; apply FcanonicNegFexpRlt with (3 := pGivesBound);
 auto.
(* Goal: Rle (FtoR radix y) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Float (Z.succ (Fnum x)) (Fexp x))) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Rlt_le; auto.
(* Goal: Fcanonic radix b (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) *)
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite <- FSuccSimpl2; auto.
(* Goal: Rle (FtoR radix (FSucc x)) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply R0RltRleSucc; auto.
(* Goal: Fcanonic radix b (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) *)
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite <- FSuccSimpl2; auto.
(* Goal: Fcanonic radix b (FSucc x) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply FSuccCanonic; auto.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
simpl in |- *; auto.
(* Goal: Z.lt (Fexp y) (Z.pred (Fexp x)) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Zsucc_lt_reg; auto.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite <- Zsucc_pred; auto with zarith.
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case y; auto.
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
intros H'6; elim H'6; intros H'7 H'8; clear H'6; apply Rlt_le.
(* Goal: Rlt (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
Contradict H'8; rewrite H'4.
(* Goal: not (Z.lt (Z.opp (nNormMin radix precision)) (Fnum y)) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Zle_not_lt.
(* Goal: Z.le (Fnum y) (Z.opp (nNormMin radix precision)) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
replace (Fnum y) with (- Zabs (Fnum y))%Z.
(* Goal: Z.le (Z.opp (Z.abs (Fnum y))) (Z.opp (nNormMin radix precision)) *)
(* Goal: @eq Z (Z.opp (Z.abs (Fnum y))) (Fnum y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Zle_Zopp.
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum y)) *)
(* Goal: @eq Z (Z.opp (Z.abs (Fnum y))) (Fnum y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply pNormal_absolu_min with (3 := pGivesBound); auto.
(* Goal: Fnormal radix b y *)
(* Goal: @eq Z (Z.opp (Z.abs (Fnum y))) (Fnum y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case H'1; auto.
(* Goal: forall _ : Fsubnormal radix b y, Fnormal radix b y *)
(* Goal: @eq Z (Z.opp (Z.abs (Fnum y))) (Fnum y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
intros H'6; Contradict H'5; rewrite H'7; auto with float.
(* Goal: @eq Z (Fexp y) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: @eq Z (Z.opp (Z.abs (Fnum y))) (Fnum y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply FsubnormalFexp with (1 := H'6).
(* Goal: @eq Z (Z.opp (Z.abs (Fnum y))) (Fnum y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite Zabs_eq_opp.
(* Goal: @eq Z (Z.opp (Z.opp (Fnum y))) (Fnum y) *)
(* Goal: Z.le (Fnum y) Z0 *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
ring.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply R0LeFnum with (radix := radix); auto with zarith.
(* Goal: Rle (FtoR radix y) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Float (Z.succ (Fnum x)) (Fexp x))) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Rlt_le; auto.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FSuccSimpl4; auto.
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case FcanonicLtNeg with (p := x) (q := y) (3 := pGivesBound); auto.
(* Goal: Rle (FtoR radix y) (IZR Z0) *)
(* Goal: forall _ : Z.lt (Fexp y) (Fexp x), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Rlt_le; auto with real.
(* Goal: Rle (FtoR radix y) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Float (Z.succ (Fnum x)) (Fexp x))) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
intros H'5; apply Rlt_le; auto.
unfold FtoRradix in |- *; apply FcanonicNegFexpRlt with (3 := pGivesBound);
 auto.
(* Goal: Rle (FtoR radix y) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Float (Z.succ (Fnum x)) (Fexp x))) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Rlt_le; auto.
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite <- FSuccSimpl4; auto.
(* Goal: Rle (FtoR radix (FSucc x)) (IZR Z0) *)
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply R0RltRleSucc; auto.
(* Goal: Fcanonic radix b (Float (Z.succ (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite <- FSuccSimpl4; auto.
(* Goal: Fcanonic radix b (FSucc x) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply FSuccCanonic; auto.
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
intros H'5; elim H'5; intros H'6 H'7; clear H'5.
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
replace y with (Float (Fnum y) (Fexp y)).
(* Goal: Rle (FtoRradix (Float (Z.succ (Fnum x)) (Fexp x))) (FtoRradix (Float (Fnum y) (Fexp y))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite H'6.
generalize Fle_Zle; unfold Fle, FtoRradix in |- *; intros H'8; apply H'8;
 clear H'8; auto with zarith arith.
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case y; auto.
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
apply Zlt_not_eq.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zlt_trans with 0%Z; auto with zarith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply R0LtFnum with (radix := radix); auto with zarith.
(* Goal: Z.lt Z0 (pPred (vNum b)) *)
unfold pPred in |- *; apply Zlt_succ_pred.
replace (Zsucc 0) with (Z_of_nat 1);
 [ apply (vNumbMoreThanOne radix) with (precision := precision)
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 | simpl in |- * ]; auto with zarith.
Qed.
 
Theorem FSuccProp :
 forall x y : float,
 Fcanonic radix b x -> Fcanonic radix b y -> (x < y)%R -> (FSucc x <= y)%R.
(* Goal: forall (x y : float) (_ : Fcanonic radix b x) (_ : Fcanonic radix b y) (_ : Rlt (FtoRradix x) (FtoRradix y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
intros x y H' H'0 H'1; case (Rle_or_lt 0 x); intros H'2.
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply FSuccPropPos; auto.
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply FSuccPropNeg; auto.
Qed.
 
Theorem FSuccZleEq :
 forall p q : float,
 (p <= q)%R -> (q < FSucc p)%R -> (Fexp p <= Fexp q)%Z -> p = q :>R.
(* Goal: forall (p q : float) (_ : Rle (FtoRradix p) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
intros p q H'.
generalize (Z_eq_bool_correct (Fnum p) (pPred (vNum b)));
(* Goal: forall _ : not (@eq Z (Fnum a) (pPred (vNum b))), Rle (FtoRradix (Float (Z.succ (Fnum a)) (Fexp a))) (IZR Z0) *)
 case (Z_eq_bool (Fnum p) (pPred (vNum b))); intros H'0.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
rewrite FSuccSimpl1; simpl in |- *; auto with arith.
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (Float (nNormMin radix precision) (Z.succ (Fexp p))))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
intros H'1 H'2.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
replace p with (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q).
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (FtoRradix q) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q) p *)
unfold FtoRradix in |- *; rewrite FshiftCorrect; auto with real.
cut (Fexp (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q) = Fexp p);
 [ intros Eq0 | idtac ].
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply floatEq; auto.
(* Goal: @eq Z (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum p) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply sym_equal; apply Zeq_Zs; auto.
(* Goal: Z.le (Fnum p) (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FshiftCorrect; auto.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
replace (Zsucc (Fnum p)) with (Fnum (Fshift radix 1 (FSucc p))); auto.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum (Float (Z.succ (Fnum p)) (Fexp p))) *)
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
repeat rewrite FshiftCorrect; auto.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
rewrite FSuccSimpl1; simpl in |- *; auto with arith.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
rewrite FSuccSimpl1; simpl in |- *; auto with arith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite inj_abs; auto with zarith.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
rewrite FSuccSimpl1; simpl in |- *; auto with arith.
(* Goal: @eq Z (Z.mul (nNormMin radix precision) (Z.mul radix (Zpos xH))) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite Z.mul_1_r.
(* Goal: @eq Z (Z.mul (nNormMin radix precision) radix) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite H'0.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix (Z.succ (Z.pred (nNormMin radix precision))))) *)
unfold pPred in |- *; rewrite <- Zsucc_pred.
rewrite (PosNormMin radix) with (precision := precision); auto with zarith;
 apply Zmult_comm.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite inj_abs; auto with zarith.
generalize (Z_eq_bool_correct (Fnum p) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum p) (- nNormMin radix precision)); 
 intros H'1.
generalize (Z_eq_bool_correct (Fexp p) (- dExp b));
 case (Z_eq_bool (Fexp p) (- dExp b)); intros H'2.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
pattern p at 1 in |- *; replace p with (Float (Fnum p) (Fexp p)).
(* Goal: @eq Z (Fnum (FSucc (Float (Fnum p) (Fexp p)))) (Z.succ (Fnum p)) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite H'1; rewrite H'2.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) (FtoR radix (Float (Z.of_nat (S O)) (Fexp (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl3; auto with arith.
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p))))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
intros H'3 H'4.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
replace p with (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q).
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (FtoRradix q) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q) p *)
unfold FtoRradix in |- *; rewrite FshiftCorrect; auto with real.
cut (Fexp (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q) = Fexp p);
 [ intros Eq0 | idtac ].
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply floatEq; auto.
(* Goal: @eq Z (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum p) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply sym_equal; apply Zeq_Zs; auto.
(* Goal: Z.le (Fnum p) (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FshiftCorrect; auto.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
replace (Zsucc (Fnum p)) with (Fnum (FSucc p)); auto.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum (FSucc p)) *)
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
pattern p at 2 in |- *; replace p with (Float (Fnum p) (Fexp p)).
(* Goal: @eq Z (Fnum (FSucc (Float (Fnum p) (Fexp p)))) (Z.succ (Fnum p)) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite H'1; rewrite H'2.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) (FtoR radix (Float (Z.of_nat (S O)) (Fexp (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl3; auto with arith.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Z.opp (Z.of_N (dExp b))))) q)) (Fnum (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite <- H'2.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum (Float (Z.succ (Fnum p)) (Fexp p))) *)
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FshiftCorrect; auto.
(* Goal: Rlt (FtoR radix q) (FtoR radix (Float (Z.succ (Z.opp (nNormMin radix precision))) (Fexp p))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite H'2; auto.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case p; simpl in |- *; auto.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
pattern p at 1 in |- *; replace p with (Float (Fnum p) (Fexp p)).
(* Goal: @eq Z (Fnum (FSucc (Float (Fnum p) (Fexp p)))) (Z.succ (Fnum p)) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite H'1; rewrite H'2.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) (FtoR radix (Float (Z.of_nat (S O)) (Fexp (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl3; auto with arith.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case p; simpl in |- *; auto.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite inj_abs; auto with zarith.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
case p; simpl in |- *; auto.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Z.of_nat (S O)) (Z.pred (Fexp p)))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl2; auto with arith.
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p))))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
intros H'3 H'4.
unfold FtoRradix in |- *; rewrite <- FshiftCorrect with (n := 1) (x := p);
 auto.
replace (Fshift radix 1 p) with
 (Fshift radix (S (Zabs_nat (Fexp q - Fexp p))) q).
(* Goal: @eq R (FtoR radix (Fshift radix (S (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))) q)) (FtoR radix q) *)
(* Goal: @eq float (Fshift radix (S (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))) q) (Fshift radix (S O) p) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
repeat rewrite FshiftCorrect; auto with real.
cut
 (Fexp (Fshift radix (S (Zabs_nat (Fexp q - Fexp p))) q) =
  Fexp (Fshift radix 1 p)); [ intros Eq0 | idtac ].
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply floatEq; auto.
(* Goal: @eq Z (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum p) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply sym_equal; apply Zeq_Zs; auto.
(* Goal: Z.le (Fnum p) (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
repeat rewrite FshiftCorrect; auto.
(* Goal: Z.lt (Fnum (Fshift radix (S (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))) q)) (Z.succ (Fnum (Fshift radix (S O) p))) *)
(* Goal: @eq Z (Fexp (Fshift radix (S (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))) q)) (Fexp (Fshift radix (S O) p)) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
replace (Zsucc (Fnum (Fshift radix 1 p))) with (Fnum (FSucc p)); auto.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum (Float (Z.succ (Fnum p)) (Fexp p))) *)
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
repeat rewrite FshiftCorrect; auto.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Z.of_nat (S O)) (Z.pred (Fexp p)))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl2; auto with arith.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Z.of_nat (S O)) (Z.pred (Fexp p)))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl2; auto with arith.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Z.of_nat (S O)) (Z.pred (Fexp p)))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl2; auto with arith.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq Z (Z.opp (pPred (vNum b))) (Z.succ (Z.mul (Fnum p) (Z.mul radix (Zpos xH)))) *)
(* Goal: @eq Z (Fexp (Fshift radix (S (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))) q)) (Fexp (Fshift radix (S O) p)) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite Z.mul_1_r; auto.
unfold pPred in |- *;
 rewrite (PosNormMin radix) with (precision := precision); 
 auto with zarith; rewrite H'1.
(* Goal: @eq Z (Z.opp (Z.pred (Z.mul radix (nNormMin radix precision)))) (Z.succ (Z.mul (Z.opp (nNormMin radix precision)) radix)) *)
(* Goal: @eq Z (Fexp (Fshift radix (S (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))) q)) (Fexp (Fshift radix (S O) p)) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.opp (Z.pred (Z.mul radix (nNormMin radix precision)))) (Z.succ (Z.opp (Z.mul (nNormMin radix precision) radix))) *)
(* Goal: @eq Z (Fexp (Fshift radix (S (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))) q)) (Fexp (Fshift radix (S O) p)) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
rewrite (Zmult_comm radix).
(* Goal: @eq Z (Z.opp (Z.pred (Z.mul (nNormMin radix precision) radix))) (Z.succ (Z.opp (Z.mul (nNormMin radix precision) radix))) *)
(* Goal: @eq Z (Fexp (Fshift radix (S (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))) q)) (Fexp (Fshift radix (S O) p)) *)
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (FSucc p))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
apply Zopp_Zpred_Zs.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
unfold Fshift in |- *; simpl in |- *.
replace (Zpos (P_of_succ_nat (Zabs_nat (Fexp q - Fexp p))))
 with (Zsucc (Fexp q - Fexp p)).
(* Goal: @eq Z (Z.opp (Z.opp (Fnum y))) (Fnum y) *)
(* Goal: Z.le (Fnum y) Z0 *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
unfold Zsucc, Zpred in |- *; ring.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite <- (inj_abs (Fexp q - Fexp p)); auto with zarith.
(* Goal: Z.lt (Fexp (Float (Fnum y) (Fexp y))) (Fexp (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) *)
(* Goal: @eq float (Float (Fnum y) (Fexp y)) y *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)))) (FtoRradix y) *)
(* Goal: Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: not (@eq Z (Fnum x) (pPred (vNum b))) *)
rewrite <- inj_S; simpl in |- *; auto.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite inj_abs; auto with zarith.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FSuccSimpl4; auto.
(* Goal: forall (_ : Rlt (FtoRradix q) (FtoRradix (Float (Z.succ (Fnum p)) (Fexp p)))) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
intros H'2 H'3.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
replace p with (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q).
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (FtoRradix q) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q) p *)
unfold FtoRradix in |- *; rewrite FshiftCorrect; auto with real.
cut (Fexp (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q) = Fexp p);
 [ intros Eq0 | idtac ].
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply floatEq; auto.
(* Goal: @eq Z (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum p) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply sym_equal; apply Zeq_Zs; auto.
(* Goal: Z.le (Fnum p) (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FshiftCorrect; auto.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
replace (Zsucc (Fnum p)) with (Fnum (FSucc p)); auto.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FSuccSimpl4; auto.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum (Float (Z.succ (Fnum p)) (Fexp p))) *)
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
repeat rewrite FshiftCorrect; auto.
(* Goal: @eq Z (Fnum (FSucc p)) (Z.succ (Fnum p)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
rewrite FSuccSimpl4; auto.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
rewrite inj_abs; auto with zarith.
Qed.
 
Definition FNSucc x := FSucc (Fnormalize radix b precision x).
 
Theorem FNSuccCanonic :
 forall a : float, Fbounded b a -> Fcanonic radix b (FNSucc a).
(* Goal: forall (a : float) (_ : Fbounded b a), Fcanonic radix b (FNSucc a) *)
intros a H'; unfold FNSucc in |- *.
(* Goal: Fcanonic radix b (FSucc (Fnormalize radix b precision a)) *)
apply FSuccCanonic; auto with float.
Qed.
 
Theorem FNSuccLt : forall a : float, (a < FNSucc a)%R.
(* Goal: forall a : float, Rlt (FtoRradix a) (FtoRradix (FNSucc a)) *)
intros a; unfold FNSucc in |- *.
unfold FtoRradix in |- *;
 rewrite <- (FnormalizeCorrect _ radixMoreThanOne b precision a).
(* Goal: Rlt (FtoR radix (Fnormalize radix b precision a)) (FtoR radix (FSucc (Fnormalize radix b precision a))) *)
apply FSuccLt; auto.
Qed.
 
Theorem FNSuccProp :
 forall x y : float,
 Fbounded b x -> Fbounded b y -> (x < y)%R -> (FNSucc x <= y)%R.
(* Goal: forall (x y : float) (_ : Fbounded b x) (_ : Fbounded b y) (_ : Rlt (FtoRradix x) (FtoRradix y)), Rle (FtoRradix (FNSucc x)) (FtoRradix y) *)
intros x y H' H'0 H'1; unfold FNSucc in |- *.
(* Goal: Rle (FtoRradix (FSucc (Fnormalize radix b precision x))) (FtoRradix y) *)
replace (FtoRradix y) with (FtoRradix (Fnormalize radix b precision y)).
(* Goal: Rle (FtoRradix (FSucc (Fnormalize radix b precision x))) (FtoRradix (Fnormalize radix b precision y)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision y)) (FtoRradix y) *)
apply FSuccProp; auto with float.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision y)) (FtoRradix y) *)
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision y)) (FtoRradix y) *)
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
Qed.
 
Theorem FNSuccEq :
 forall p q : float,
 Fbounded b p -> Fbounded b q -> p = q :>R -> FNSucc p = FNSucc q.
(* Goal: forall (p q : float) (_ : Fbounded b p) (_ : Fbounded b q) (_ : @eq R (FtoRradix p) (FtoRradix q)), @eq float (FNSucc p) (FNSucc q) *)
intros p q H' H'0 H'1; unfold FNSucc in |- *.
replace (Fnormalize radix b precision p) with
 (Fnormalize radix b precision q); auto.
apply FcanonicUnique with (radix := radix) (b := b) (precision := precision);
 auto with float.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision q)) (FtoR radix (Fnormalize radix b precision p)) *)
repeat rewrite FnormalizeCorrect; auto.
Qed.
End suc.
Hint Resolve FSuccNormPos FBoundedSuc FSuccSubnormal FSuccNegCanonic
  FSuccCanonic FSuccLt FSuccPropPos R0RltRleSucc FSuccPropNeg FSuccProp
  FNSuccCanonic FNSuccLt: float.
Section suc1.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
 
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionNotZero : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Theorem nNormMimLtvNum : (nNormMin radix precision < pPred (vNum b))%Z.
unfold pPred in |- *;
 rewrite PosNormMin with (radix := radix) (precision := precision);
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
 auto with zarith.
(* Goal: Z.lt (nNormMin radix precision) (Z.pred (Z.mul radix (nNormMin radix precision))) *)
apply Zlt_le_trans with (Zpred (2 * nNormMin radix precision)).
replace (Zpred (2 * nNormMin radix precision)) with
 (Zpred (nNormMin radix precision) + nNormMin radix precision)%Z;
 [ idtac | unfold Zpred in |- *; ring ].
pattern (nNormMin radix precision) at 1 in |- *;
 replace (nNormMin radix precision) with (0 + nNormMin radix precision)%Z;
 [ idtac | ring ].
(* Goal: Z.lt (Z.add Z0 (nNormMin radix precision)) (Z.add (Z.pred (nNormMin radix precision)) (nNormMin radix precision)) *)
(* Goal: Z.le (Z.pred (Z.mul (Zpos (xO xH)) (nNormMin radix precision))) (Z.pred (Z.mul radix (nNormMin radix precision))) *)
apply Zplus_lt_compat_r; auto.
(* Goal: Z.lt Z0 (Z.pred (nNormMin radix precision)) *)
(* Goal: Z.le (Z.pred (Z.mul (Zpos (xO xH)) (nNormMin radix precision))) (Z.pred (Z.mul radix (nNormMin radix precision))) *)
apply Zlt_succ_pred.
(* Goal: Z.lt (Z.succ Z0) (nNormMin radix precision) *)
(* Goal: Z.le (Z.pred (Z.mul (Zpos (xO xH)) (nNormMin radix precision))) (Z.pred (Z.mul radix (nNormMin radix precision))) *)
replace (Zsucc 0) with (Z_of_nat 1); [ idtac | simpl in |- *; auto ].
(* Goal: Z.lt (Z.of_nat (S O)) (nNormMin radix precision) *)
(* Goal: Z.le (Z.pred (Z.mul (Zpos (xO xH)) (nNormMin radix precision))) (Z.pred (Z.mul radix (nNormMin radix precision))) *)
rewrite <- (Zpower_nat_O radix); unfold nNormMin in |- *.
(* Goal: Z.lt (Zpower_nat radix O) (Zpower_nat radix (Init.Nat.pred precision)) *)
(* Goal: Z.le (Z.pred (Z.mul (Zpos (xO xH)) (nNormMin radix precision))) (Z.pred (Z.mul radix (nNormMin radix precision))) *)
apply Zpower_nat_monotone_lt. assumption. now apply lt_pred.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zle_Zpred_Zpred. apply Zle_Zmult_comp_r; auto with zarith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Z.lt_le_incl; apply nNormPos; auto with zarith.
Qed.
 
Theorem FSucFSucMid :
 forall p : float,
 Fnum (FSucc b radix precision p) <> nNormMin radix precision ->
 Fnum (FSucc b radix precision p) <> (- nNormMin radix precision)%Z ->
 Fminus radix (FSucc b radix precision (FSucc b radix precision p))
   (FSucc b radix precision p) = Fminus radix (FSucc b radix precision p) p
 :>R.
(* Goal: forall (p : float) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
intros p.
generalize (Z_eq_bool_correct (Fnum p) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum p) (- nNormMin radix precision)); 
 intros H'1.
generalize (Z_eq_bool_correct (Fexp p) (- dExp b));
 case (Z_eq_bool (Fexp p) (- dExp b)); intros H'2.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccDiff2 with (2 := H'1); auto with arith.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Z.of_nat (S O)) (Fexp p))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
replace p with (Float (Fnum p) (Fexp p)).
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Fnum p) (Fexp p)))) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Fnum p) (Fexp p)))) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision (Float (Fnum p) (Fexp p)))) (FSucc b radix precision (Float (Fnum p) (Fexp p))))) (FtoR radix (Float (Z.of_nat (S O)) (Fexp (Float (Fnum p) (Fexp p))))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
repeat (rewrite H'1; rewrite H'2).
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))))) (FSucc b radix precision (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) (FtoR radix (Float (Z.of_nat (S O)) (Fexp (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl3; auto with arith.
(* Goal: forall (_ : not (@eq Z (Fnum (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b)))))) (FtoR radix (Float (Z.of_nat (S O)) (Fexp (Float (Z.opp (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))))))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccDiff1 with (2 := pGivesBound); auto with arith.
(* Goal: not (@eq Z (Fnum (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.opp (Z.of_N (dExp b))))) (Z.opp (nNormMin radix precision))) *)
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
simpl in |- *; auto with zarith.
(* Goal: @eq float (Float (Fnum p) (Fexp p)) p *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply floatEq; auto.
unfold FtoRradix in |- *; rewrite FSuccDiff3 with (x := p) (3 := pGivesBound);
 auto with arith.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Z.of_nat (S O)) (Z.pred (Fexp p)))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
rewrite FSuccSimpl2; auto with arith.
(* Goal: @eq R (FtoR radix (Fminus radix (FSucc b radix precision (Float (Z.succ (Fnum p)) (Fexp p))) (Float (Z.succ (Fnum p)) (Fexp p)))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
rewrite FSuccDiff1; simpl in |- *; auto with arith.
(* Goal: not (@eq Z (Z.opp (pPred (vNum b))) (Z.opp (nNormMin radix precision))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply Zlt_not_eq; auto.
(* Goal: Z.lt (Z.opp (pPred (vNum b))) (Z.opp (nNormMin radix precision)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply Zlt_Zopp; auto.
(* Goal: Z.lt (nNormMin radix precision) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoRradix (Fminus radix (FSucc b radix precision p) p)) *)
apply nNormMimLtvNum; auto.
unfold FtoRradix in |- *; rewrite FSuccDiff1 with (x := p); simpl in |- *;
 auto with arith.
generalize (Z_eq_bool_correct (Fnum p) (pPred (vNum b)));
 case (Z_eq_bool (Fnum p) (pPred (vNum b))); intros H'2.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
rewrite FSuccSimpl1; simpl in |- *; auto with arith.
(* Goal: forall (_ : not (@eq Z (nNormMin radix precision) (nNormMin radix precision))) (_ : not (@eq Z (nNormMin radix precision) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (Float (nNormMin radix precision) (Z.succ (Fexp p)))) (Float (nNormMin radix precision) (Z.succ (Fexp p))))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
intros H'; case H'; auto.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoR radix (Fminus radix (FSucc b radix precision (FSucc b radix precision p)) (FSucc b radix precision p))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
rewrite FSuccSimpl4; simpl in |- *; auto with arith.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision (Fnormalize radix b precision p))) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision (Fnormalize radix b precision p))) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (Fnormalize radix b precision (FSucc b radix precision (Fnormalize radix b precision p)))) (FSucc b radix precision (Fnormalize radix b precision p)))) (FtoRradix (Fminus radix (FSucc b radix precision (Fnormalize radix b precision p)) p)) *)
intros H' H'0.
(* Goal: @eq R (FtoR radix (Fminus radix (FSucc b radix precision (Float (Z.succ (Fnum p)) (Fexp p))) (Float (Z.succ (Fnum p)) (Fexp p)))) (FtoR radix (Float (Zpos xH) (Fexp p))) *)
rewrite FSuccDiff1; simpl in |- *; auto with arith.
Qed.
 
Theorem FNSuccFNSuccMid :
 forall p : float,
 Fbounded b p ->
 Fnum (FNSucc b radix precision p) <> nNormMin radix precision ->
 Fnum (FNSucc b radix precision p) <> (- nNormMin radix precision)%Z ->
 Fminus radix (FNSucc b radix precision (FNSucc b radix precision p))
   (FNSucc b radix precision p) = Fminus radix (FNSucc b radix precision p) p
 :>R.
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : not (@eq Z (Fnum (FNSucc b radix precision p)) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FNSucc b radix precision p)) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FNSucc b radix precision (FNSucc b radix precision p)) (FNSucc b radix precision p))) (FtoRradix (Fminus radix (FNSucc b radix precision p) p)) *)
intros p Fb; unfold FNSucc in |- *.
(* Goal: forall (_ : not (@eq Z (Fnum (FSucc b radix precision (Fnormalize radix b precision p))) (nNormMin radix precision))) (_ : not (@eq Z (Fnum (FSucc b radix precision (Fnormalize radix b precision p))) (Z.opp (nNormMin radix precision)))), @eq R (FtoRradix (Fminus radix (FSucc b radix precision (Fnormalize radix b precision (FSucc b radix precision (Fnormalize radix b precision p)))) (FSucc b radix precision (Fnormalize radix b precision p)))) (FtoRradix (Fminus radix (FSucc b radix precision (Fnormalize radix b precision p)) p)) *)
intros H' H'0.
rewrite
 FcanonicFnormalizeEq
                     with
                     (p := 
                       FSucc b radix precision
                         (Fnormalize radix b precision p));
 auto with float arith.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision (FSucc b radix precision (Fnormalize radix b precision p))) (FSucc b radix precision (Fnormalize radix b precision p)))) (FtoRradix (Fminus radix (FSucc b radix precision (Fnormalize radix b precision p)) p)) *)
rewrite FSucFSucMid; auto.
unfold FtoRradix in |- *; repeat rewrite Fminus_correct;
 auto with float arith.
(* Goal: @eq R (Rminus (FtoR radix (FSucc b radix precision (Fnormalize radix b precision p))) (FtoR radix (Fnormalize radix b precision p))) (Rminus (FtoR radix (FSucc b radix precision (Fnormalize radix b precision p))) (FtoR radix p)) *)
(* Goal: Z.lt Z0 radix *)
(* Goal: Z.lt Z0 radix *)
rewrite FnormalizeCorrect; auto.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zlt_trans with 1%Z; auto with zarith.
(* Goal: Z.lt (Zpos xH) radix *)
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Fcanonic radix b (Float (nNormMin radix precision) (Z.succ (Fexp x))) *)
(* Goal: forall _ : Z.lt (Fexp x) (Fexp y), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
(* Goal: forall _ : and (@eq Z (Fexp x) (Fexp y)) (Z.lt (Fnum x) (Fnum y)), Rle (FtoRradix (FSucc x)) (FtoRradix y) *)
apply Zlt_trans with 1%Z; auto with zarith.
Qed.

End suc1.
Hint Resolve nNormMimLtvNum: float.
