(****************************************************************************
                                                                             
          IEEE754  :  FPred                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export FSucc.
Section pred.
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 : precision <> 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Definition FPred (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 (Zpred (Fnum x)) (Fexp x)
          | false => Float (pPred (vNum b)) (Zpred (Fexp x))
          end
      | false => Float (Zpred (Fnum x)) (Fexp x)
      end
  end.
 
Theorem FPredSimpl1 :
 forall x : float,
 Fnum x = (- pPred (vNum b))%Z ->
 FPred x = Float (- nNormMin radix precision) (Zsucc (Fexp x)).
(* Goal: forall (x : float) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (FPred x) (Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x))) *)
intros x H'; unfold FPred 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) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)) (Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x))) *)
intros H'0; Contradict H'0; auto.
Qed.
 
Theorem FPredSimpl2 :
 forall x : float,
 Fnum x = nNormMin radix precision ->
 Fexp x <> (- dExp b)%Z -> FPred x = Float (pPred (vNum b)) (Zpred (Fexp x)).
(* Goal: forall (x : float) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))), @eq float (FPred x) (Float (Z.pred (Fnum x)) (Fexp x)) *)
intros x H' H'0; unfold FPred 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) (Z.opp (pPred (vNum b))), @eq float (Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x))) (Float (pPred (vNum b)) (Z.pred (Fexp x))) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)) (Float (pPred (vNum b)) (Z.pred (Fexp x))) *)
intros H'1; absurd (0%nat < Fnum x)%Z; auto with zarith arith.
apply Zle_not_lt; rewrite H'1; replace (Z_of_nat 0) with (- (0))%Z;
 [ apply Zle_Zopp | simpl in |- *; auto ].
(* Goal: Z.le Z0 (pPred (vNum b)) *)
(* Goal: Z.lt (Z.of_nat O) (Fnum x) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)) (Float (pPred (vNum b)) (Z.pred (Fexp x))) *)
unfold pPred in |- *; apply Zle_Zpred; red in |- *; simpl in |- *; auto.
(* Goal: Z.lt (Z.of_nat O) (Fnum x) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)) (Float (pPred (vNum b)) (Z.pred (Fexp x))) *)
rewrite H'.
(* Goal: Z.lt (Z.of_nat O) (nNormMin radix precision) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)) (Float (pPred (vNum b)) (Z.pred (Fexp x))) *)
apply nNormPos; 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.pred (Fnum x)) (Fexp x)) (Float (pPred (vNum b)) (Z.pred (Fexp x))) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (nNormMin radix precision)), @eq float (Float (Z.pred (Fnum x)) (Fexp x)) (Float (pPred (vNum b)) (Z.pred (Fexp x))) *)
intros H'3; Contradict H'0; auto.
(* Goal: forall _ : not (@eq Z (Fnum x) (nNormMin radix precision)), @eq float (Float (Z.pred (Fnum x)) (Fexp x)) (Float (pPred (vNum b)) (Z.pred (Fexp x))) *)
intros H'2; Contradict H'2; auto.
Qed.
 
Theorem FPredSimpl3 :
 FPred (Float (nNormMin radix precision) (- dExp b)) =
 Float (Zpred (nNormMin radix precision)) (- dExp b).
(* Goal: @eq float (FPred (Float (nNormMin radix precision) (Z.opp (Z.of_N (dExp b))))) (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) *)
unfold FPred 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 (nNormMin radix precision) (Z.opp (pPred (vNum b))), @eq float (Float (Z.opp (nNormMin radix precision)) (Z.succ (Z.opp (Z.of_N (dExp b))))) (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: forall _ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (nNormMin radix precision) (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.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))) else Float (pPred (vNum b)) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) *)
intros H'0; absurd (0 < pPred (vNum b))%Z; auto with zarith arith.
(* Goal: not (Z.lt Z0 (pPred (vNum b))) *)
(* Goal: Z.lt Z0 (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (nNormMin radix precision) (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.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))) else Float (pPred (vNum b)) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) *)
rewrite <- (Zopp_involutive (pPred (vNum b))); rewrite <- H'0.
apply Zle_not_lt; replace 0%Z with (- (0))%Z;
 [ apply Zle_Zopp | simpl in |- *; auto ].
(* Goal: Z.le Z0 (nNormMin radix precision) *)
(* Goal: Z.lt Z0 (pPred (vNum b)) *)
(* Goal: forall _ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (nNormMin radix precision) (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.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))) else Float (pPred (vNum b)) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) *)
apply Zlt_le_weak; apply nNormPos; auto with float zarith.
unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *;
 auto with float zarith.
(* Goal: Z.lt (Zpos xH) (Zpos (vNum b)) *)
(* Goal: forall _ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (nNormMin radix precision) (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.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b))) else Float (pPred (vNum b)) (Z.pred (Z.opp (Z.of_N (dExp b)))) else Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) *)
simpl in |- *; apply vNumbMoreThanOne with (3 := pGivesBound); auto.
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 (nNormMin radix precision) (nNormMin radix precision)), @eq float (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) *)
intros H'1; Contradict H'1; auto.
(* Goal: forall _ : not (@eq Z (nNormMin radix precision) (nNormMin radix precision)), @eq float (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) *)
intros H'1; Contradict H'1; auto.
Qed.
 
Theorem FPredSimpl4 :
 forall x : float,
 Fnum x <> (- pPred (vNum b))%Z ->
 Fnum x <> nNormMin radix precision ->
 FPred x = Float (Zpred (Fnum x)) (Fexp x).
(* Goal: forall (x : float) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))), @eq float (FPred x) (Float (Z.pred (Fnum x)) (Fexp x)) *)
intros x H' H'0; unfold FPred 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) (Z.opp (pPred (vNum b))), @eq float (Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x))) (Float (Z.pred (Fnum x)) (Fexp x)) *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)) (Float (Z.pred (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) (nNormMin radix precision), @eq float (if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x))) (Float (Z.pred (Fnum x)) (Fexp x)) *)
intros H'2; Contradict H'0; auto.
Qed.
 
Theorem FPredFopFSucc :
 forall x : float, FPred x = Fopp (FSucc b radix precision (Fopp x)).
(* Goal: forall x : float, @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
intros x.
generalize (Z_eq_bool_correct (Fnum x) (- pPred (vNum b)));
 case (Z_eq_bool (Fnum x) (- pPred (vNum b))); intros H'1.
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
rewrite FPredSimpl1; auto; rewrite FSuccSimpl1; auto.
(* Goal: @eq Z (Fnum (Fopp x)) (pPred (vNum b)) *)
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
unfold Fopp in |- *; simpl in |- *; rewrite H'1; auto with zarith.
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)); intros H'3.
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
replace x with (Float (Fnum x) (Fexp x)).
rewrite H'2; rewrite H'3; rewrite FPredSimpl3; unfold Fopp in |- *;
 simpl in |- *; rewrite FSuccSimpl3; simpl in |- *; 
 auto.
(* Goal: @eq float (Float (Z.pred (nNormMin radix precision)) (Z.opp (Z.of_N (dExp b)))) (Float (Z.opp (Z.succ (Z.opp (nNormMin radix precision)))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
rewrite <- Zopp_Zpred_Zs; rewrite Zopp_involutive; auto.
(* Goal: @eq Z (Z.opp (Fnum x)) (Fnum (Fopp x)) *)
case x; simpl in |- *; auto.
rewrite FPredSimpl2; auto; rewrite FSuccSimpl2; unfold Fopp in |- *;
 simpl in |- *; try rewrite Zopp_involutive; 
 auto.
(* Goal: @eq Z (Z.opp (Fnum x)) (Z.opp (nNormMin radix precision)) *)
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
rewrite H'2; auto.
(* Goal: @eq float (FPred x) (Fopp (FSucc b radix precision (Fopp x))) *)
rewrite FPredSimpl4; auto; rewrite FSuccSimpl4; auto.
unfold Fopp in |- *; simpl in |- *; rewrite <- Zopp_Zpred_Zs;
 rewrite Zopp_involutive; auto.
unfold Fopp in |- *; simpl in |- *; Contradict H'1; rewrite <- H'1;
 rewrite Zopp_involutive; auto.
(* Goal: not (@eq Z (Fnum (Fopp x)) (Z.opp (nNormMin radix precision))) *)
unfold Fopp in |- *; simpl in |- *; Contradict H'2; auto with zarith.
Qed.
 
Theorem FPredDiff1 :
 forall x : float,
 Fnum x <> nNormMin radix precision ->
 Fminus radix x (FPred x) = Float 1%nat (Fexp x) :>R.
(* Goal: forall (x : float) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))), @eq R (FtoRradix (Fminus radix x (FPred x))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
intros x H'; rewrite (FPredFopFSucc x).
(* Goal: @eq R (FtoRradix (Fminus radix x (Fopp (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
pattern x at 1 in |- *; rewrite <- (Fopp_Fopp x).
(* Goal: @eq R (FtoRradix (Fminus radix (Fopp (Fopp x)) (Fopp (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
rewrite <- Fopp_Fminus_dist.
(* Goal: @eq R (FtoRradix (Fopp (Fminus radix (Fopp x) (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
rewrite Fopp_Fminus.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision (Fopp x)) (Fopp x))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
unfold FtoRradix in |- *; rewrite FSuccDiff1; auto.
(* Goal: not (@eq Z (Fnum (Fopp x)) (Z.opp (nNormMin radix precision))) *)
replace (Fnum (Fopp x)) with (- Fnum x)%Z.
Contradict H'; rewrite <- (Zopp_involutive (Fnum x)); rewrite H';
 auto with zarith.
(* Goal: @eq Z (Z.opp (Fnum x)) (Fnum (Fopp x)) *)
case x; simpl in |- *; auto.
Qed.
 
Theorem FPredDiff2 :
 forall x : float,
 Fnum x = nNormMin radix precision ->
 Fexp x = (- dExp b)%Z -> Fminus radix x (FPred x) = Float 1%nat (Fexp x) :>R.
(* Goal: forall (x : float) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))), @eq R (FtoRradix (Fminus radix x (FPred x))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
intros x H' H'0; rewrite (FPredFopFSucc x).
(* Goal: @eq R (FtoRradix (Fminus radix x (Fopp (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
pattern x at 1 in |- *; rewrite <- (Fopp_Fopp x).
(* Goal: @eq R (FtoRradix (Fminus radix (Fopp (Fopp x)) (Fopp (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
rewrite <- Fopp_Fminus_dist.
(* Goal: @eq R (FtoRradix (Fopp (Fminus radix (Fopp x) (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
rewrite Fopp_Fminus.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision (Fopp x)) (Fopp x))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
unfold FtoRradix in |- *; rewrite FSuccDiff2; auto.
(* Goal: @eq Z (Fnum (Fopp x)) (Z.opp (nNormMin radix precision)) *)
rewrite <- H'; case x; auto.
Qed.
 
Theorem FPredDiff3 :
 forall x : float,
 Fnum x = nNormMin radix precision ->
 Fexp x <> (- dExp b)%Z ->
 Fminus radix x (FPred x) = Float 1%nat (Zpred (Fexp x)) :>R.
(* Goal: forall (x : float) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))), @eq R (FtoRradix (Fminus radix x (FPred x))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
intros x H' H'0; rewrite (FPredFopFSucc x).
(* Goal: @eq R (FtoRradix (Fminus radix x (Fopp (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
pattern x at 1 in |- *; rewrite <- (Fopp_Fopp x).
(* Goal: @eq R (FtoRradix (Fminus radix (Fopp (Fopp x)) (Fopp (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
rewrite <- Fopp_Fminus_dist.
(* Goal: @eq R (FtoRradix (Fopp (Fminus radix (Fopp x) (FSucc b radix precision (Fopp x))))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
rewrite Fopp_Fminus.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision (Fopp x)) (Fopp x))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp x)))) *)
unfold FtoRradix in |- *; rewrite FSuccDiff3; auto.
(* Goal: @eq Z (Fnum (Fopp x)) (Z.opp (nNormMin radix precision)) *)
rewrite <- H'; case x; auto.
Qed.
 
Theorem FBoundedPred : forall f : float, Fbounded b f -> Fbounded b (FPred f).
(* Goal: forall (f : float) (_ : Fbounded b f), Fbounded b (FPred f) *)
intros f H'; rewrite (FPredFopFSucc f); auto with float.
Qed.
 
Theorem FPredCanonic :
 forall a : float, Fcanonic radix b a -> Fcanonic radix b (FPred a).
(* Goal: forall (a : float) (_ : Fcanonic radix b a), Fcanonic radix b (FPred a) *)
intros a H'.
(* Goal: Fcanonic radix b (FPred a) *)
rewrite FPredFopFSucc; auto with float.
Qed.
 
Theorem FPredLt : forall a : float, (FPred a < a)%R.
(* Goal: forall a : float, Rlt (FtoRradix (FPred a)) (FtoRradix a) *)
intros a; rewrite FPredFopFSucc.
(* Goal: Rlt (FtoRradix (Fopp (FSucc b radix precision (Fopp a)))) (FtoRradix a) *)
pattern a at 2 in |- *; rewrite <- (Fopp_Fopp a).
(* Goal: Rlt (FtoR radix (Fopp x)) (IZR Z0) *)
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
(* Goal: Rlt (Ropp (FtoR radix (FSucc b radix precision (Fopp a)))) (Ropp (Ropp (FtoR radix a))) *)
apply Ropp_lt_contravar.
(* Goal: Rlt (Ropp (FtoR radix a)) (FtoR radix (FSucc b radix precision (Fopp a))) *)
rewrite <- Fopp_correct; auto with float.
Qed.
 
Theorem R0RltRlePred : forall x : float, (0 < x)%R -> (0 <= FPred x)%R.
(* Goal: forall (x : float) (_ : Rlt (IZR Z0) (FtoRradix x)), Rle (IZR Z0) (FtoRradix (FPred x)) *)
intros x H'; rewrite FPredFopFSucc.
(* Goal: Rlt (FtoR radix (Fopp x)) (IZR Z0) *)
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
(* Goal: Rlt (Ropp (FtoR radix x)) (IZR Z0) *)
replace 0%R with (-0)%R; auto with real.
(* Goal: Rle (Ropp (FtoR radix (Fopp x))) (Ropp (FtoR radix (FSucc b radix precision (Fopp y)))) *)
apply Ropp_le_contravar.
(* Goal: Rle (FtoR radix (FSucc b radix precision (Fopp x))) (IZR Z0) *)
apply R0RltRleSucc; auto.
(* Goal: Rlt (FtoR radix (Fopp x)) (IZR Z0) *)
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
(* Goal: Rlt (Ropp (FtoR radix x)) (IZR Z0) *)
replace 0%R with (-0)%R; auto with real.
Qed.
 
Theorem FPredProp :
 forall x y : float,
 Fcanonic radix b x -> Fcanonic radix b y -> (x < y)%R -> (x <= FPred y)%R.
(* Goal: forall (x y : float) (_ : Fcanonic radix b x) (_ : Fcanonic radix b y) (_ : Rlt (FtoRradix x) (FtoRradix y)), Rle (FtoRradix x) (FtoRradix (FPred y)) *)
intros x y H' H'0 H'1; rewrite FPredFopFSucc.
(* Goal: Rle (FtoRradix x) (FtoRradix (Fopp (FSucc b radix precision (Fopp y)))) *)
rewrite <- (Fopp_Fopp x).
(* Goal: Rle (FtoRradix (Fopp (Fopp x))) (FtoRradix (Fopp (FSucc b radix precision (Fopp y)))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct with (x := Fopp x).
rewrite Fopp_correct with (x := FSucc b radix precision (Fopp y));
 auto with float real.
(* Goal: Rle (Ropp (FtoR radix (Fopp x))) (Ropp (FtoR radix (FSucc b radix precision (Fopp y)))) *)
apply Ropp_le_contravar.
(* Goal: Rle (FtoR radix (FSucc b radix precision (Fopp y))) (FtoR radix (Fopp x)) *)
apply FSuccProp; auto with float.
(* Goal: Rle (FtoR radix (Fopp p)) (FtoR radix (Fopp q)) *)
(* Goal: Rlt (FtoR radix (Fopp q)) (FtoR radix (FSucc b radix precision (Fopp p))) *)
repeat rewrite Fopp_correct; auto with real.
Qed.
 
Theorem FPredZleEq :
 forall p q : float,
 (FPred p < q)%R -> (q <= p)%R -> (Fexp p <= Fexp q)%Z -> p = q :>R.
(* Goal: forall (p q : float) (_ : Rlt (FtoRradix (FPred p)) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)) (_ : Z.le (Fexp p) (Fexp q)), @eq R (FtoRradix p) (FtoRradix q) *)
intros p q H' H'0 H'1.
rewrite <- (Ropp_involutive p); rewrite <- (Ropp_involutive q);
 apply Ropp_eq_compat.
(* Goal: @eq R (Ropp (FtoRradix p)) (Ropp (FtoRradix q)) *)
unfold FtoRradix in |- *; repeat rewrite <- Fopp_correct.
(* Goal: @eq R (FtoR radix (Fopp p)) (FtoR radix (Fopp q)) *)
apply FSuccZleEq with (b := b) (precision := precision); auto.
(* Goal: Rle (FtoR radix (Fopp p)) (FtoR radix (Fopp q)) *)
(* Goal: Rlt (FtoR radix (Fopp q)) (FtoR radix (FSucc b radix precision (Fopp p))) *)
repeat rewrite Fopp_correct; auto with real.
(* Goal: Rlt (FtoR radix (Fopp q)) (FtoR radix (FSucc b radix precision (Fopp p))) *)
apply Ropp_lt_cancel.
repeat rewrite <- Fopp_correct; rewrite <- FPredFopFSucc; rewrite Fopp_Fopp;
 auto.
Qed.
 
Definition FNPred (x : float) := FPred (Fnormalize radix b precision x).
 
Theorem FNPredFopFNSucc :
 forall x : float, FNPred x = Fopp (FNSucc b radix precision (Fopp x)).
(* Goal: forall x : float, @eq float (FNPred x) (Fopp (FNSucc b radix precision (Fopp x))) *)
intros x; unfold FNPred, FNSucc in |- *; auto.
(* Goal: @eq float (FPred (Fnormalize radix b precision x)) (Fopp (FSucc b radix precision (Fnormalize radix b precision (Fopp x)))) *)
rewrite Fnormalize_Fopp; auto.
(* Goal: @eq float (FPred (Fnormalize radix b precision x)) (Fopp (FSucc b radix precision (Fopp (Fnormalize radix b precision x)))) *)
apply FPredFopFSucc; auto.
Qed.
 
Theorem FNPredCanonic :
 forall a : float, Fbounded b a -> Fcanonic radix b (FNPred a).
(* Goal: forall (a : float) (_ : Fbounded b a), Fcanonic radix b (FNPred a) *)
intros a H'; unfold FNPred in |- *.
(* Goal: Fcanonic radix b (FPred (Fnormalize radix b precision a)) *)
apply FPredCanonic; auto with float.
Qed.
 
Theorem FNPredLt : forall a : float, (FNPred a < a)%R.
(* Goal: forall a : float, Rlt (FtoRradix (FNPred a)) (FtoRradix a) *)
intros a; unfold FNPred in |- *.
unfold FtoRradix in |- *;
 rewrite <- (FnormalizeCorrect _ radixMoreThanOne b precision a).
(* Goal: Rlt (FtoR radix (FPred (Fnormalize radix b precision a))) (FtoR radix (Fnormalize radix b precision a)) *)
apply FPredLt; auto.
Qed.
 
Theorem FNPredProp :
 forall x y : float,
 Fbounded b x -> Fbounded b y -> (x < y)%R -> (x <= FNPred y)%R.
(* Goal: forall (x y : float) (_ : Fbounded b x) (_ : Fbounded b y) (_ : Rlt (FtoRradix x) (FtoRradix y)), Rle (FtoRradix x) (FtoRradix (FNPred y)) *)
intros x y H' H'0 H'1; unfold FNPred in |- *.
(* Goal: Rle (FtoRradix x) (FtoRradix (FPred (Fnormalize radix b precision y))) *)
replace (FtoRradix x) with (FtoRradix (Fnormalize radix b precision x)).
(* Goal: Rle (FtoRradix (Fnormalize radix b precision x)) (FtoRradix (FPred (Fnormalize radix b precision y))) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision x)) (FtoRradix x) *)
apply FPredProp; auto with float.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision x)) (FtoRradix x) *)
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision x)) (FtoRradix x) *)
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
Qed.
 
Theorem FPredSuc :
 forall x : float,
 Fcanonic radix b x -> FPred (FSucc b radix precision x) = x.
(* Goal: forall (x : float) (_ : Fcanonic radix b x), @eq float (FSucc b radix precision (FPred x)) x *)
intros x H; unfold FPred, FSucc in |- *.
(* Goal: @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
cut (Fbounded b x); [ intros Fb0 | apply FcanonicBound with (1 := H) ].
generalize (Z_eq_bool_correct (Fnum x) (pPred (vNum b)));
 case (Z_eq_bool (Fnum x) (pPred (vNum b))); simpl in |- *.
generalize (Z_eq_bool_correct (nNormMin radix precision) (- pPred (vNum b)));
 case (Z_eq_bool (nNormMin radix precision) (- pPred (vNum b)));
 simpl in |- *.
(* Goal: forall (_ : @eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b)))) (_ : @eq Z (Fnum x) (pPred (vNum b))), @eq float (Float (Z.opp (nNormMin radix precision)) (Z.succ (Z.succ (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (nNormMin radix precision) (nNormMin radix precision) then if Z_eq_bool (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (nNormMin radix precision)) (Z.succ (Fexp x)) else Float (pPred (vNum b)) (Z.pred (Z.succ (Fexp x))) else Float (Z.pred (nNormMin radix precision)) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (Fnum (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))) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp (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)))) else if Z_eq_bool (Fnum (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))) (nNormMin radix precision) then if Z_eq_bool (Fexp (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))) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum (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)))) (Fexp (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))) else Float (pPred (vNum b)) (Z.pred (Fexp (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)))) else Float (Z.pred (Fnum (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)))) (Fexp (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)))) x *)
intros H'; Contradict H'; apply sym_not_equal; apply Zlt_not_eq; auto.
(* Goal: Z.lt (Z.opp (pPred (vNum b))) (nNormMin radix precision) *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (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.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
apply Zlt_le_trans with (- 0%nat)%Z.
apply Zlt_Zopp; unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *;
 apply vNumbMoreThanOne with (3 := pGivesBound); auto.
(* Goal: Z.le (Z.opp (Z.of_nat O)) (nNormMin radix precision) *)
(* Goal: forall (_ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (nNormMin radix precision) (nNormMin radix precision) then if Z_eq_bool (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (nNormMin radix precision)) (Z.succ (Fexp x)) else Float (pPred (vNum b)) (Z.pred (Z.succ (Fexp x))) else Float (Z.pred (nNormMin radix precision)) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (Fnum (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))) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp (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)))) else if Z_eq_bool (Fnum (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))) (nNormMin radix precision) then if Z_eq_bool (Fexp (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))) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum (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)))) (Fexp (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))) else Float (pPred (vNum b)) (Z.pred (Fexp (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)))) else Float (Z.pred (Fnum (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)))) (Fexp (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)))) x *)
simpl in |- *; apply Zlt_le_weak; apply nNormPos; auto.
generalize
 (Z_eq_bool_correct (nNormMin radix precision) (nNormMin radix precision));
 case (Z_eq_bool (nNormMin radix precision) (nNormMin radix precision));
 simpl in |- *.
generalize (Z_eq_bool_correct (Zsucc (Fexp x)) (- dExp b));
 case (Z_eq_bool (Zsucc (Fexp x)) (- dExp b)); simpl in |- *.
(* Goal: forall (_ : @eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
intros H' H'0 H'1 H'2; absurd (- dExp b <= Fexp x)%Z; auto with float.
(* Goal: not (Z.le (Z.opp (Z.of_N (dExp b))) (Fexp x)) *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (nNormMin radix precision) (nNormMin radix precision)) (_ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fnum x) (pPred (vNum b))), @eq float (Float (pPred (vNum b)) (Z.pred (Z.succ (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (nNormMin radix precision) (nNormMin radix precision))) (_ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fnum x) (pPred (vNum b))), @eq float (Float (Z.pred (nNormMin radix precision)) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (Fnum (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))) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp (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)))) else if Z_eq_bool (Fnum (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))) (nNormMin radix precision) then if Z_eq_bool (Fexp (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))) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum (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)))) (Fexp (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))) else Float (pPred (vNum b)) (Z.pred (Fexp (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)))) else Float (Z.pred (Fnum (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)))) (Fexp (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)))) x *)
rewrite <- H'; auto with float zarith.
replace (Zpred (Zsucc (Fexp x))) with (Fexp x);
 [ idtac | unfold Zsucc, Zpred in |- *; ring ]; auto.
(* Goal: forall (_ : not (@eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (nNormMin radix precision) (nNormMin radix precision)) (_ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fnum x) (pPred (vNum b))), @eq float (Float (pPred (vNum b)) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (nNormMin radix precision) (nNormMin radix precision))) (_ : not (@eq Z (nNormMin radix precision) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fnum x) (pPred (vNum b))), @eq float (Float (Z.pred (nNormMin radix precision)) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (pPred (vNum b))), @eq float (if Z_eq_bool (Fnum (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))) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp (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)))) else if Z_eq_bool (Fnum (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))) (nNormMin radix precision) then if Z_eq_bool (Fexp (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))) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum (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)))) (Fexp (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))) else Float (pPred (vNum b)) (Z.pred (Fexp (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)))) else Float (Z.pred (Fnum (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)))) (Fexp (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)))) x *)
intros H' H'0 H'1 H'2; rewrite <- H'2; auto.
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.succ (Fnum x)) (nNormMin radix precision)) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
apply floatEq; auto.
(* Goal: forall (_ : not (@eq Z (pPred (vNum b)) (pPred (vNum b)))) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
intros H'; case H'; auto.
generalize (Z_eq_bool_correct (Fnum x) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum x) (- nNormMin radix precision)); 
 simpl in |- *.
generalize (Z_eq_bool_correct (Fexp x) (- dExp b));
 case (Z_eq_bool (Fexp x) (- dExp b)); simpl in |- *.
generalize (Z_eq_bool_correct (Zsucc (Fnum x)) (- pPred (vNum b)));
 case (Z_eq_bool (Zsucc (Fnum x)) (- pPred (vNum b))); 
 simpl in |- *.
(* Goal: forall (_ : @eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b)))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.opp (pPred (vNum b))) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (Z.opp (pPred (vNum b))) (nNormMin radix precision) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x)) else Float (pPred (vNum b)) (Z.pred (Z.pred (Fexp x))) else Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H0 H1 H2; absurd (Zsucc (Fnum x) <= Fnum x)%Z; auto with zarith.
(* Goal: Z.le (Z.succ (Fnum x)) (Fnum x) *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.opp (pPred (vNum b))) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (Z.opp (pPred (vNum b))) (nNormMin radix precision) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x)) else Float (pPred (vNum b)) (Z.pred (Z.pred (Fexp x))) else Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
rewrite H0; rewrite H2; (apply Zle_Zopp; auto with float arith).
(* Goal: Z.le (nNormMin radix precision) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.opp (pPred (vNum b))) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (Z.opp (pPred (vNum b))) (nNormMin radix precision) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x)) else Float (pPred (vNum b)) (Z.pred (Z.pred (Fexp x))) else Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
unfold pPred in |- *; apply Zle_Zpred; apply ZltNormMinVnum; auto with zarith.
generalize (Z_eq_bool_correct (Zsucc (Fnum x)) (nNormMin radix precision));
 case (Z_eq_bool (Zsucc (Fnum x)) (nNormMin radix precision)); 
 simpl in |- *.
(* Goal: forall (_ : @eq Z (Z.succ (Fnum x)) (nNormMin radix precision)) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.opp (pPred (vNum b))) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (Z.opp (pPred (vNum b))) (nNormMin radix precision) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x)) else Float (pPred (vNum b)) (Z.pred (Z.pred (Fexp x))) else Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H' H'0 H'1 H'2; Contradict H'2.
(* Goal: not (Z.le (Z.opp (Z.of_N (dExp b))) (Fexp x)) *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
rewrite <- H'; auto with zarith.
replace (Zpred (Zsucc (Fnum x))) with (Fnum x);
 [ idtac | unfold Zsucc, Zpred in |- *; ring ]; auto.
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.succ (Fnum x)) (nNormMin radix precision)) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H' H'0 H'1 H'2 H'3; apply floatEq; auto.
generalize (Z_eq_bool_correct (- pPred (vNum b)) (- pPred (vNum b)));
 case (Z_eq_bool (- pPred (vNum b)) (- pPred (vNum b))); 
 auto.
(* Goal: forall (_ : @eq Z (Z.opp (pPred (vNum b))) (Z.opp (pPred (vNum b)))) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.opp (nNormMin radix precision)) (Z.succ (Z.pred (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (Z.opp (pPred (vNum b))) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.opp (pPred (vNum b))) (nNormMin radix precision) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x)) else Float (pPred (vNum b)) (Z.pred (Z.pred (Fexp x))) else Float (Z.pred (Z.opp (pPred (vNum b)))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H' H'0 H'1 H'2; rewrite <- H'1.
replace (Zsucc (Zpred (Fexp x))) with (Fexp x);
 [ idtac | unfold Zsucc, Zpred in |- *; ring ]; auto.
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.succ (Fnum x)) (nNormMin radix precision)) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
apply floatEq; auto.
(* Goal: forall (_ : not (@eq Z (pPred (vNum b)) (pPred (vNum b)))) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
intros H'; case H'; auto.
generalize (Z_eq_bool_correct (Zsucc (Fnum x)) (- pPred (vNum b)));
 case (Z_eq_bool (Zsucc (Fnum x)) (- pPred (vNum b))); 
 simpl in |- *.
(* Goal: forall (_ : @eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H'; absurd (- pPred (vNum b) <= Fnum x)%Z; auto with float.
(* Goal: not (Z.le (Z.opp (Z.of_N (dExp b))) (Fexp x)) *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
rewrite <- H'; auto with zarith.
(* Goal: Z.le (Z.opp (pPred (vNum b))) (Fnum x) *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (if Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Z.succ (Fnum x))) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
apply Zle_Zabs_inv1; auto with float.
(* Goal: Z.le (Z.abs (Fnum x)) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
unfold pPred in |- *; apply Zle_Zpred; auto with float.
generalize (Z_eq_bool_correct (Zsucc (Fnum x)) (nNormMin radix precision));
 case (Z_eq_bool (Zsucc (Fnum x)) (nNormMin radix precision)); 
 simpl in |- *.
generalize (Z_eq_bool_correct (Fexp x) (- dExp b));
 case (Z_eq_bool (Fexp x) (- dExp b)); simpl in |- *.
(* Goal: forall (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Z.succ (Fnum x)) (nNormMin radix precision)) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.succ (Fnum x)) (nNormMin radix precision)) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H' H'0 H'1 H'2 H'3.
replace (Zpred (Zsucc (Fnum x))) with (Fnum x);
 [ idtac | unfold Zsucc, Zpred in |- *; ring ]; auto.
(* Goal: @eq float (Float (Fnum x) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.succ (Fnum x)) (nNormMin radix precision)) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
apply floatEq; auto.
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.succ (Fnum x)) (nNormMin radix precision)) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H' H'0 H'1 H'2 H'3; case H.
(* Goal: forall _ : Fnormal radix b x, @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall _ : Fsubnormal radix b x, @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H'4; absurd (nNormMin radix precision <= Zabs (Fnum x))%Z.
replace (Fnum x) with (Zpred (Zsucc (Fnum x)));
 [ idtac | unfold Zsucc, Zpred in |- *; ring ]; auto.
(* Goal: not (Z.le (nNormMin radix precision) (Z.abs (Z.succ (Z.pred (Fnum x))))) *)
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
rewrite H'0.
(* Goal: not (Z.le (nNormMin radix precision) (Z.abs (Z.pred (nNormMin radix precision)))) *)
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: forall _ : Fsubnormal radix b x, @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
apply Zlt_not_le; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.le Z0 (Z.pred (nNormMin radix precision)) *)
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: forall _ : Fsubnormal radix b x, @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
apply Zle_Zpred; apply nNormPos; auto with float zarith.
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
apply pNormal_absolu_min with (b := b); auto.
(* Goal: forall _ : Fsubnormal radix b x, @eq float (Float (pPred (vNum b)) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fnum x)) (nNormMin radix precision))) (_ : not (@eq Z (Z.succ (Fnum x)) (Z.opp (pPred (vNum b))))) (_ : not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Fnum x) (pPred (vNum b)))), @eq float (Float (Z.pred (Z.succ (Fnum x))) (Fexp x)) x *)
intros H'4; Contradict H'; apply FsubnormalFexp with (1 := H'4).
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
intros H' H'0 H'1 H'2; apply floatEq; simpl in |- *; auto.
(* Goal: @eq Z (Z.succ (Z.pred (Fnum x))) (Fnum x) *)
unfold Zpred, Zsucc in |- *; ring.
Qed.
 
Theorem FSucPred :
 forall x : float,
 Fcanonic radix b x -> FSucc b radix precision (FPred x) = x.
(* Goal: forall (x : float) (_ : Fcanonic radix b x), @eq float (FSucc b radix precision (FPred x)) x *)
intros x H; unfold FPred, FSucc in |- *.
(* Goal: @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (Z.opp (pPred (vNum b))) then Float (Z.opp (nNormMin radix precision)) (Z.succ (Fexp x)) else if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
cut (Fbounded b x); [ intros Fb0 | apply FcanonicBound with (1 := H) ].
generalize (Z_eq_bool_correct (Fnum x) (- pPred (vNum b)));
 case (Z_eq_bool (Fnum x) (- pPred (vNum b))); simpl in |- *.
generalize (Z_eq_bool_correct (- nNormMin radix precision) (pPred (vNum b)));
 case (Z_eq_bool (- nNormMin radix precision) (pPred (vNum b)));
 simpl in |- *.
(* Goal: forall (_ : @eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (nNormMin radix precision) (Z.succ (Z.succ (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (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.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
intros H'; Contradict H'; apply Zlt_not_eq; auto.
(* Goal: Z.lt (Z.opp (nNormMin radix precision)) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (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.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
rewrite <- (Zopp_involutive (pPred (vNum b))); apply Zlt_Zopp.
(* Goal: Z.lt (Z.opp (pPred (vNum b))) (nNormMin radix precision) *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (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.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
apply Zlt_le_trans with (- 0%nat)%Z.
(* Goal: Z.lt (Z.opp (pPred (vNum b))) (Z.opp (Z.of_nat O)) *)
(* Goal: Z.le (Z.opp (Z.of_nat O)) (nNormMin radix precision) *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (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.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
apply Zlt_Zopp; unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *.
(* Goal: Z.lt (Zpos xH) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_nat O)) (nNormMin radix precision) *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (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.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
apply (vNumbMoreThanOne radix) with (precision := precision); auto.
(* Goal: Z.le (Z.opp (Z.of_nat O)) (nNormMin radix precision) *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (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.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x))) else Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
simpl in |- *; apply Zlt_le_weak; apply nNormPos; auto with zarith arith.
generalize
 (Z_eq_bool_correct (- nNormMin radix precision) (- nNormMin radix precision));
 case (Z_eq_bool (- nNormMin radix precision) (- nNormMin radix precision));
 simpl in |- *.
generalize (Z_eq_bool_correct (Zsucc (Fexp x)) (- dExp b));
 case (Z_eq_bool (Zsucc (Fexp x)) (- dExp b)); simpl in |- *.
(* Goal: forall (_ : @eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
intros H' H'0 H'1 H'2; absurd (- dExp b <= Fexp x)%Z; auto with float.
(* Goal: not (Z.le (Z.opp (Z.of_N (dExp b))) (Fexp x)) *)
(* Goal: forall (_ : not (@eq Z (Z.succ (Fexp x)) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Z.succ (Fexp x)))) x *)
(* Goal: forall (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.opp (nNormMin radix precision)) (pPred (vNum b)))) (_ : @eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (Float (Z.succ (Z.opp (nNormMin radix precision))) (Z.succ (Fexp x))) x *)
(* Goal: forall _ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b)))), @eq float (if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else if Z_eq_bool (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x))) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) else Float (Z.succ (Fnum (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) (Fexp (if Z_eq_bool (Fnum x) (nNormMin radix precision) then if Z_eq_bool (Fexp x) (Z.opp (Z.of_N (dExp b))) then Float (Z.pred (Fnum x)) (Fexp x) else Float (pPred (vNum b)) (Z.pred (Fexp x)) else Float (Z.pred (Fnum x)) (Fexp x)))) x *)
rewrite <- H'; auto with zarith.
intros H' H'0 H'1 H'2; rewrite <- H'2; apply floatEq; simpl in |- *; auto;
 unfold Zsucc, Zpred in |- *; ring.
(* Goal: forall (_ : not (@eq Z (pPred (vNum b)) (pPred (vNum b)))) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
intros H'; case H'; auto.
generalize (Z_eq_bool_correct (Fnum x) (nNormMin radix precision));
 case (Z_eq_bool (Fnum x) (nNormMin radix precision)); 
 simpl in |- *.
generalize (Z_eq_bool_correct (Fexp x) (- dExp b));
 case (Z_eq_bool (Fexp x) (- dExp b)); simpl in |- *.
generalize (Z_eq_bool_correct (Zpred (Fnum x)) (pPred (vNum b)));
 case (Z_eq_bool (Zpred (Fnum x)) (pPred (vNum b))); 
 simpl in |- *.
intros H' H'0 H'1 H'2; absurd (nNormMin radix precision <= pPred (vNum b))%Z;
 auto with float.
(* Goal: not (Z.le (nNormMin radix precision) (pPred (vNum b))) *)
(* Goal: Z.le (nNormMin radix precision) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
rewrite <- H'; rewrite H'1; auto with zarith.
(* Goal: Z.le (nNormMin radix precision) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
rewrite <- H'1; auto with float.
(* Goal: Z.le (Fnum x) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
apply Zle_Zabs_inv2; auto with float zarith.
(* Goal: Z.le (Z.abs (Fnum x)) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
unfold pPred in |- *; apply Zle_Zpred; auto with float.
generalize (Z_eq_bool_correct (Zpred (Fnum x)) (- nNormMin radix precision));
 case (Z_eq_bool (Zpred (Fnum x)) (- nNormMin radix precision));
 simpl in |- *.
intros H' H'0 H'1 H'2 H'3;
 absurd (Zpred (nNormMin radix precision) = (- nNormMin radix precision)%Z);
 auto with zarith.
intros H' H'0 H'1 H'2 H'3; apply floatEq; simpl in |- *; auto;
(* Goal: @eq Z (Z.succ (Z.pred (Fnum x))) (Fnum x) *)
 unfold Zpred, Zsucc in |- *; ring.
generalize (Z_eq_bool_correct (pPred (vNum b)) (pPred (vNum b)));
 case (Z_eq_bool (pPred (vNum b)) (pPred (vNum b))); 
 auto.
intros H' H'0 H'1 H'2; rewrite <- H'1; apply floatEq; simpl in |- *; auto;
(* Goal: @eq Z (Z.succ (Z.pred (Fnum x))) (Fnum x) *)
 unfold Zpred, Zsucc in |- *; ring.
(* Goal: forall (_ : not (@eq Z (pPred (vNum b)) (pPred (vNum b)))) (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
intros H'; case H'; auto.
generalize (Z_eq_bool_correct (Zpred (Fnum x)) (pPred (vNum b)));
 case (Z_eq_bool (Zpred (Fnum x)) (pPred (vNum b))); 
 simpl in |- *.
(* Goal: forall (_ : @eq Z (Z.pred (Fnum x)) (pPred (vNum b))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (nNormMin radix precision) (Z.succ (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
intros H'; absurd (Fnum x <= pPred (vNum b))%Z; auto with float.
(* Goal: not (Z.le (Fnum x) (pPred (vNum b))) *)
(* Goal: Z.le (Fnum x) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
rewrite <- H'.
(* Goal: not (Z.le (Fnum x) (Z.pred (Fnum x))) *)
(* Goal: Z.le (Fnum x) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
apply Zlt_not_le; apply Zlt_pred; auto.
(* Goal: Z.le (Z.abs (Fnum x)) (pPred (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : @eq Z (Fexp x) (Z.opp (Z.of_N (dExp b)))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Fnum x) (nNormMin radix precision)) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (pPred (vNum b)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Z.pred (Fexp x))) else if Z_eq_bool (pPred (vNum b)) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Z.pred (Fexp x)) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.opp (pPred (vNum b))) (Z.pred (Z.pred (Fexp x))) else Float (Z.succ (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (if Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)) then Float (nNormMin radix precision) (Z.succ (Fexp x)) else if Z_eq_bool (Z.pred (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 (Z.pred (Fnum x))) (Fexp x) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x)) else Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
apply Zle_Zabs_inv2; unfold pPred in |- *; apply Zle_Zpred; auto with float.
generalize (Z_eq_bool_correct (Zpred (Fnum x)) (- nNormMin radix precision));
 case (Z_eq_bool (Zpred (Fnum x)) (- nNormMin radix precision));
 simpl in |- *.
generalize (Z_eq_bool_correct (Fexp x) (- dExp b));
 case (Z_eq_bool (Fexp x) (- dExp b)); simpl in |- *.
intros H' H'0 H'1 H'2 H'3; apply floatEq; simpl in |- *; auto;
 unfold Zsucc, Zpred in |- *; ring.
(* Goal: forall (_ : not (@eq Z (Fexp x) (Z.opp (Z.of_N (dExp b))))) (_ : @eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
intros H' H'0 H'1 H'2 H'3; case H; intros C0.
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
absurd (nNormMin radix precision <= Zabs (Fnum x))%Z; auto with float.
replace (Fnum x) with (Zsucc (Zpred (Fnum x)));
 [ idtac | unfold Zsucc, Zpred in |- *; ring ].
(* Goal: not (Z.le (nNormMin radix precision) (Z.abs (Z.succ (Z.pred (Fnum x))))) *)
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
rewrite H'0.
(* Goal: not (Z.le (nNormMin radix precision) (Z.abs (Z.succ (Z.opp (nNormMin radix precision))))) *)
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
rewrite <- Zopp_Zpred_Zs; rewrite Zabs_Zopp.
(* Goal: not (Z.le (nNormMin radix precision) (Z.abs (Z.pred (nNormMin radix precision)))) *)
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
rewrite Zabs_eq; auto with zarith.
(* Goal: Z.le Z0 (Z.pred (nNormMin radix precision)) *)
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
apply Zle_Zpred; simpl in |- *; apply nNormPos; auto with float zarith.
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum x)) *)
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
apply pNormal_absolu_min with (b := b); auto.
(* Goal: @eq float (Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp x))) x *)
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
Contradict H'; apply FsubnormalFexp with (1 := C0).
(* Goal: forall (_ : not (@eq Z (Z.pred (Fnum x)) (Z.opp (nNormMin radix precision)))) (_ : not (@eq Z (Z.pred (Fnum x)) (pPred (vNum b)))) (_ : not (@eq Z (Fnum x) (nNormMin radix precision))) (_ : not (@eq Z (Fnum x) (Z.opp (pPred (vNum b))))), @eq float (Float (Z.succ (Z.pred (Fnum x))) (Fexp x)) x *)
intros H' H'0 H'1 H'2; apply floatEq; simpl in |- *; auto.
(* Goal: @eq Z (Z.succ (Z.pred (Fnum x))) (Fnum x) *)
unfold Zpred, Zsucc in |- *; ring.
Qed.
 
Theorem FNPredSuc :
 forall x : float,
 Fbounded b x -> FNPred (FNSucc b radix precision x) = x :>R.
(* Goal: forall (x : float) (_ : Fbounded b x), @eq R (FtoRradix (FNPred (FNSucc b radix precision x))) (FtoRradix x) *)
intros x H'; unfold FNPred in |- *; rewrite FcanonicFnormalizeEq; auto.
(* Goal: @eq R (FtoRradix (FPred (FNSucc b radix precision x))) (FtoRradix x) *)
(* Goal: Fcanonic radix b (FNSucc b radix precision x) *)
unfold FNSucc in |- *; rewrite FPredSuc; auto.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision x)) (FtoRradix x) *)
(* Goal: Fcanonic radix b (Fnormalize radix b precision x) *)
(* Goal: Fcanonic radix b (FNPred x) *)
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
(* Goal: Fcanonic radix b (Fnormalize radix b precision x) *)
(* Goal: Fcanonic radix b (FNPred x) *)
apply FnormalizeCanonic; auto.
(* Goal: Fcanonic radix b (FNSucc b radix precision (FNPred x)) *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision (FNPred x))) (FtoR radix x) *)
apply FNSuccCanonic; auto.
Qed.
 
Theorem FNPredSucEq :
 forall x : float,
 Fcanonic radix b x -> FNPred (FNSucc b radix precision x) = x.
(* Goal: forall (x : float) (_ : Fcanonic radix b x), @eq float (FNSucc b radix precision (FNPred x)) x *)
intros x H'.
(* Goal: @eq float (FNPred (FNSucc b radix precision x)) x *)
apply FcanonicUnique with (precision := precision) (5 := H'); auto.
(* Goal: Fcanonic radix b (FNPred (FNSucc b radix precision x)) *)
(* Goal: @eq R (FtoR radix (FNPred (FNSucc b radix precision x))) (FtoR radix x) *)
apply FNPredCanonic; auto with float.
(* Goal: Fbounded b x *)
apply FcanonicBound with (radix := radix); auto.
(* Goal: Fcanonic radix b (FNSucc b radix precision (FNPred x)) *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision (FNPred x))) (FtoR radix x) *)
apply FNSuccCanonic; auto.
(* Goal: Fbounded b x *)
apply FcanonicBound with (radix := radix); auto.
(* Goal: @eq R (FtoR radix (FNPred (FNSucc b radix precision x))) (FtoR radix x) *)
apply FNPredSuc; auto.
(* Goal: Fbounded b x *)
apply FcanonicBound with (radix := radix); auto.
Qed.
 
Theorem FNSucPred :
 forall x : float,
 Fbounded b x -> FNSucc b radix precision (FNPred x) = x :>R.
(* Goal: forall (x : float) (_ : Fbounded b x), @eq R (FtoRradix (FNSucc b radix precision (FNPred x))) (FtoRradix x) *)
intros x H'; unfold FNSucc in |- *; rewrite FcanonicFnormalizeEq; auto.
(* Goal: @eq R (FtoRradix (FSucc b radix precision (FNPred x))) (FtoRradix x) *)
(* Goal: Fcanonic radix b (FNPred x) *)
unfold FNPred in |- *; rewrite FSucPred; auto.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision x)) (FtoRradix x) *)
(* Goal: Fcanonic radix b (Fnormalize radix b precision x) *)
(* Goal: Fcanonic radix b (FNPred x) *)
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
(* Goal: Fcanonic radix b (Fnormalize radix b precision x) *)
(* Goal: Fcanonic radix b (FNPred x) *)
apply FnormalizeCanonic; auto.
(* Goal: Fcanonic radix b (FNPred x) *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision (FNPred x))) (FtoR radix x) *)
apply FNPredCanonic; auto.
Qed.
 
Theorem FNSucPredEq :
 forall x : float,
 Fcanonic radix b x -> FNSucc b radix precision (FNPred x) = x.
(* Goal: forall (x : float) (_ : Fcanonic radix b x), @eq float (FNSucc b radix precision (FNPred x)) x *)
intros x H'.
(* Goal: @eq float (FNSucc b radix precision (FNPred x)) x *)
apply FcanonicUnique with (5 := H') (precision := precision); auto.
(* Goal: Fcanonic radix b (FNSucc b radix precision (FNPred x)) *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision (FNPred x))) (FtoR radix x) *)
apply FNSuccCanonic; auto.
(* Goal: Fbounded b x *)
apply FcanonicBound with (radix := radix); auto.
(* Goal: Fcanonic radix b (FNPred x) *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision (FNPred x))) (FtoR radix x) *)
apply FNPredCanonic; auto.
(* Goal: Fbounded b x *)
apply FcanonicBound with (radix := radix); auto.
(* Goal: @eq R (FtoR radix (FNSucc b radix precision (FNPred x))) (FtoR radix x) *)
apply FNSucPred; auto.
(* Goal: Fbounded b x *)
apply FcanonicBound with (radix := radix); auto.
Qed.


End pred.
Hint Resolve FBoundedPred FPredCanonic FPredLt R0RltRleSucc FPredProp
  FNPredCanonic FNPredLt FNPredProp: float.