Library Float.FPred

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
  | trueFloat (- nNormMin radix precision) (Z.succ (Fexp x))
  | false
      match Z_eq_bool (Fnum x) (nNormMin radix precision) with
      | true
          match Z_eq_bool (Fexp x) (- dExp b) with
          | trueFloat (Z.pred (Fnum x)) (Fexp x)
          | falseFloat (pPred (vNum b)) (Z.pred (Fexp x))
          end
      | falseFloat (Z.pred (Fnum x)) (Fexp x)
      end
  end.

Theorem FPredSimpl1 :
  x : float,
 Fnum x = (- pPred (vNum b))%Z
 FPred x = Float (- 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.
intros H'0; Contradict H'0; auto.
Qed.

Theorem FPredSimpl2 :
  x : float,
 Fnum x = nNormMin radix precision
 Fexp x (- dExp b)%Z FPred x = Float (pPred (vNum b)) (Z.pred (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.
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 ].
unfold pPred in |- *; apply Zle_Zpred; red in |- *; simpl in |- *; auto.
rewrite H'.
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.
intros H'3; Contradict H'0; auto.
intros H'2; Contradict H'2; auto.
Qed.

Theorem FPredSimpl3 :
 FPred (Float (nNormMin radix precision) (- dExp b)) =
 Float (Z.pred (nNormMin radix precision)) (- 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.
intros H'0; absurd (0 < pPred (vNum b))%Z; auto with zarith arith.
rewrite <- (Z.opp_involutive (pPred (vNum b))); rewrite <- H'0.
apply Zle_not_lt; replace 0%Z with (- (0))%Z;
 [ apply Zle_Zopp | simpl in |- *; auto ].
apply Zlt_le_weak; apply nNormPos; auto with float zarith.
unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *;
 auto with float zarith.
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.
intros H'1; Contradict H'1; auto.
intros H'1; Contradict H'1; auto.
Qed.

Theorem FPredSimpl4 :
  x : float,
 Fnum x (- pPred (vNum b))%Z
 Fnum x nNormMin radix precision
 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.
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.
intros H'2; Contradict H'0; auto.
Qed.

Theorem FPredFopFSucc :
  x : 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.
rewrite FPredSimpl1; auto; rewrite FSuccSimpl1; auto.
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.
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.
rewrite <- Zopp_Zpred_Zs; rewrite Z.opp_involutive; auto.
case x; simpl in |- *; auto.
rewrite FPredSimpl2; auto; rewrite FSuccSimpl2; unfold Fopp in |- *;
 simpl in |- *; try rewrite Z.opp_involutive;
 auto.
rewrite H'2; auto.
rewrite FPredSimpl4; auto; rewrite FSuccSimpl4; auto.
unfold Fopp in |- *; simpl in |- *; rewrite <- Zopp_Zpred_Zs;
 rewrite Z.opp_involutive; auto.
unfold Fopp in |- *; simpl in |- *; Contradict H'1; rewrite <- H'1;
 rewrite Z.opp_involutive; auto.
unfold Fopp in |- *; simpl in |- *; Contradict H'2; auto with zarith.
Qed.

Theorem FPredDiff1 :
  x : float,
 Fnum x nNormMin radix precision
 Fminus radix x (FPred x) = Float 1%nat (Fexp x) :>R.
intros x H'; rewrite (FPredFopFSucc x).
pattern x at 1 in |- *; rewrite <- (Fopp_Fopp x).
rewrite <- Fopp_Fminus_dist.
rewrite Fopp_Fminus.
unfold FtoRradix in |- *; rewrite FSuccDiff1; auto.
replace (Fnum (Fopp x)) with (- Fnum x)%Z.
Contradict H'; rewrite <- (Z.opp_involutive (Fnum x)); rewrite H';
 auto with zarith.
case x; simpl in |- *; auto.
Qed.

Theorem FPredDiff2 :
  x : float,
 Fnum x = nNormMin radix precision
 Fexp x = (- dExp b)%Z Fminus radix x (FPred x) = Float 1%nat (Fexp x) :>R.
intros x H' H'0; rewrite (FPredFopFSucc x).
pattern x at 1 in |- *; rewrite <- (Fopp_Fopp x).
rewrite <- Fopp_Fminus_dist.
rewrite Fopp_Fminus.
unfold FtoRradix in |- *; rewrite FSuccDiff2; auto.
rewrite <- H'; case x; auto.
Qed.

Theorem FPredDiff3 :
  x : float,
 Fnum x = nNormMin radix precision
 Fexp x (- dExp b)%Z
 Fminus radix x (FPred x) = Float 1%nat (Z.pred (Fexp x)) :>R.
intros x H' H'0; rewrite (FPredFopFSucc x).
pattern x at 1 in |- *; rewrite <- (Fopp_Fopp x).
rewrite <- Fopp_Fminus_dist.
rewrite Fopp_Fminus.
unfold FtoRradix in |- *; rewrite FSuccDiff3; auto.
rewrite <- H'; case x; auto.
Qed.

Theorem FBoundedPred : f : float, Fbounded b f Fbounded b (FPred f).
intros f H'; rewrite (FPredFopFSucc f); auto with float.
Qed.

Theorem FPredCanonic :
  a : float, Fcanonic radix b a Fcanonic radix b (FPred a).
intros a H'.
rewrite FPredFopFSucc; auto with float.
Qed.

Theorem FPredLt : a : float, (FPred a < a)%R.
intros a; rewrite FPredFopFSucc.
pattern a at 2 in |- *; rewrite <- (Fopp_Fopp a).
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
apply Ropp_lt_contravar.
rewrite <- Fopp_correct; auto with float.
Qed.

Theorem R0RltRlePred : x : float, (0 < x)%R (0 FPred x)%R.
intros x H'; rewrite FPredFopFSucc.
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
replace 0%R with (-0)%R; auto with real.
apply Ropp_le_contravar.
apply R0RltRleSucc; auto.
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
replace 0%R with (-0)%R; auto with real.
Qed.

Theorem FPredProp :
  x y : float,
 Fcanonic radix b x Fcanonic radix b y (x < y)%R (x FPred y)%R.
intros x y H' H'0 H'1; rewrite FPredFopFSucc.
rewrite <- (Fopp_Fopp x).
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.
apply Ropp_le_contravar.
apply FSuccProp; auto with float.
repeat rewrite Fopp_correct; auto with real.
Qed.

Theorem FPredZleEq :
  p q : float,
 (FPred p < q)%R (q p)%R (Fexp p Fexp q)%Z p = q :>R.
intros p q H' H'0 H'1.
rewrite <- (Ropp_involutive p); rewrite <- (Ropp_involutive q);
 apply Ropp_eq_compat.
unfold FtoRradix in |- *; repeat rewrite <- Fopp_correct.
apply FSuccZleEq with (b := b) (precision := precision); auto.
repeat rewrite Fopp_correct; auto with real.
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 :
  x : float, FNPred x = Fopp (FNSucc b radix precision (Fopp x)).
intros x; unfold FNPred, FNSucc in |- *; auto.
rewrite Fnormalize_Fopp; auto.
apply FPredFopFSucc; auto.
Qed.

Theorem FNPredCanonic :
  a : float, Fbounded b a Fcanonic radix b (FNPred a).
intros a H'; unfold FNPred in |- ×.
apply FPredCanonic; auto with float.
Qed.

Theorem FNPredLt : a : float, (FNPred a < a)%R.
intros a; unfold FNPred in |- ×.
unfold FtoRradix in |- *;
 rewrite <- (FnormalizeCorrect _ radixMoreThanOne b precision a).
apply FPredLt; auto.
Qed.

Theorem FNPredProp :
  x y : float,
 Fbounded b x Fbounded b y (x < y)%R (x FNPred y)%R.
intros x y H' H'0 H'1; unfold FNPred in |- ×.
replace (FtoRradix x) with (FtoRradix (Fnormalize radix b precision x)).
apply FPredProp; auto with float.
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
Qed.

Theorem FPredSuc :
  x : float,
 Fcanonic radix b x FPred (FSucc b radix precision x) = x.
intros x H; unfold FPred, FSucc in |- ×.
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 |- ×.
intros H'; Contradict H'; apply sym_not_equal; apply Zlt_not_eq; auto.
apply Z.lt_le_trans with (- 0%nat)%Z.
apply Zlt_Zopp; unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *;
 apply vNumbMoreThanOne with (3 := pGivesBound); auto.
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 (Z.succ (Fexp x)) (- dExp b));
 case (Z_eq_bool (Z.succ (Fexp x)) (- dExp b)); simpl in |- ×.
intros H' H'0 H'1 H'2; absurd (- dExp b Fexp x)%Z; auto with float.
rewrite <- H'; auto with float zarith.
replace (Z.pred (Z.succ (Fexp x))) with (Fexp x);
 [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto.
intros H' H'0 H'1 H'2; rewrite <- H'2; auto.
apply floatEq; auto.
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 (Z.succ (Fnum x)) (- pPred (vNum b)));
 case (Z_eq_bool (Z.succ (Fnum x)) (- pPred (vNum b)));
 simpl in |- ×.
intros H0 H1 H2; absurd (Z.succ (Fnum x) Fnum x)%Z; auto with zarith.
rewrite H0; rewrite H2; (apply Zle_Zopp; auto with float arith).
unfold pPred in |- *; apply Zle_Zpred; apply ZltNormMinVnum; auto with zarith.
generalize (Z_eq_bool_correct (Z.succ (Fnum x)) (nNormMin radix precision));
 case (Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision));
 simpl in |- ×.
intros H' H'0 H'1 H'2; Contradict H'2.
rewrite <- H'; auto with zarith.
replace (Z.pred (Z.succ (Fnum x))) with (Fnum x);
 [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto.
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.
intros H' H'0 H'1 H'2; rewrite <- H'1.
replace (Z.succ (Z.pred (Fexp x))) with (Fexp x);
 [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto.
apply floatEq; auto.
intros H'; case H'; auto.
generalize (Z_eq_bool_correct (Z.succ (Fnum x)) (- pPred (vNum b)));
 case (Z_eq_bool (Z.succ (Fnum x)) (- pPred (vNum b)));
 simpl in |- ×.
intros H'; absurd (- pPred (vNum b) Fnum x)%Z; auto with float.
rewrite <- H'; auto with zarith.
apply Zle_Zabs_inv1; auto with float.
unfold pPred in |- *; apply Zle_Zpred; auto with float.
generalize (Z_eq_bool_correct (Z.succ (Fnum x)) (nNormMin radix precision));
 case (Z_eq_bool (Z.succ (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.
replace (Z.pred (Z.succ (Fnum x))) with (Fnum x);
 [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto.
apply floatEq; auto.
intros H' H'0 H'1 H'2 H'3; case H.
intros H'4; absurd (nNormMin radix precision Z.abs (Fnum x))%Z.
replace (Fnum x) with (Z.pred (Z.succ (Fnum x)));
 [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto.
rewrite H'0.
apply Zlt_not_le; rewrite Z.abs_eq; auto with zarith.
apply Zle_Zpred; apply nNormPos; auto with float zarith.
apply pNormal_absolu_min with (b := b); auto.
intros H'4; Contradict H'; apply FsubnormalFexp with (1 := H'4).
intros H' H'0 H'1 H'2; apply floatEq; simpl in |- *; auto.
unfold Z.pred, Z.succ in |- *; ring.
Qed.

Theorem FSucPred :
  x : float,
 Fcanonic radix b x FSucc b radix precision (FPred x) = x.
intros x H; unfold FPred, FSucc in |- ×.
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 |- ×.
intros H'; Contradict H'; apply Zlt_not_eq; auto.
rewrite <- (Z.opp_involutive (pPred (vNum b))); apply Zlt_Zopp.
apply Z.lt_le_trans with (- 0%nat)%Z.
apply Zlt_Zopp; unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- ×.
apply (vNumbMoreThanOne radix) with (precision := precision); auto.
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 (Z.succ (Fexp x)) (- dExp b));
 case (Z_eq_bool (Z.succ (Fexp x)) (- dExp b)); simpl in |- ×.
intros H' H'0 H'1 H'2; absurd (- dExp b Fexp x)%Z; auto with float.
rewrite <- H'; auto with zarith.
intros H' H'0 H'1 H'2; rewrite <- H'2; apply floatEq; simpl in |- *; auto;
 unfold Z.succ, Z.pred in |- *; ring.
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 (Z.pred (Fnum x)) (pPred (vNum b)));
 case (Z_eq_bool (Z.pred (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.
rewrite <- H'; rewrite H'1; auto with zarith.
rewrite <- H'1; auto with float.
apply Zle_Zabs_inv2; auto with float zarith.
unfold pPred in |- *; apply Zle_Zpred; auto with float.
generalize (Z_eq_bool_correct (Z.pred (Fnum x)) (- nNormMin radix precision));
 case (Z_eq_bool (Z.pred (Fnum x)) (- nNormMin radix precision));
 simpl in |- ×.
intros H' H'0 H'1 H'2 H'3;
 absurd (Z.pred (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;
 unfold Z.pred, Z.succ 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;
 unfold Z.pred, Z.succ in |- *; ring.
intros H'; case H'; auto.
generalize (Z_eq_bool_correct (Z.pred (Fnum x)) (pPred (vNum b)));
 case (Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b)));
 simpl in |- ×.
intros H'; absurd (Fnum x pPred (vNum b))%Z; auto with float.
rewrite <- H'.
apply Zlt_not_le; apply Zlt_pred; auto.
apply Zle_Zabs_inv2; unfold pPred in |- *; apply Zle_Zpred; auto with float.
generalize (Z_eq_bool_correct (Z.pred (Fnum x)) (- nNormMin radix precision));
 case (Z_eq_bool (Z.pred (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 Z.succ, Z.pred in |- *; ring.
intros H' H'0 H'1 H'2 H'3; case H; intros C0.
absurd (nNormMin radix precision Z.abs (Fnum x))%Z; auto with float.
replace (Fnum x) with (Z.succ (Z.pred (Fnum x)));
 [ idtac | unfold Z.succ, Z.pred in |- *; ring ].
rewrite H'0.
rewrite <- Zopp_Zpred_Zs; rewrite Zabs_Zopp.
rewrite Z.abs_eq; auto with zarith.
apply Zle_Zpred; simpl in |- *; apply nNormPos; auto with float zarith.
apply pNormal_absolu_min with (b := b); auto.
Contradict H'; apply FsubnormalFexp with (1 := C0).
intros H' H'0 H'1 H'2; apply floatEq; simpl in |- *; auto.
unfold Z.pred, Z.succ in |- *; ring.
Qed.

Theorem FNPredSuc :
  x : float,
 Fbounded b x FNPred (FNSucc b radix precision x) = x :>R.
intros x H'; unfold FNPred in |- *; rewrite FcanonicFnormalizeEq; auto.
unfold FNSucc in |- *; rewrite FPredSuc; auto.
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
apply FnormalizeCanonic; auto.
apply FNSuccCanonic; auto.
Qed.

Theorem FNPredSucEq :
  x : float,
 Fcanonic radix b x FNPred (FNSucc b radix precision x) = x.
intros x H'.
apply FcanonicUnique with (precision := precision) (5 := H'); auto.
apply FNPredCanonic; auto with float.
apply FcanonicBound with (radix := radix); auto.
apply FNSuccCanonic; auto.
apply FcanonicBound with (radix := radix); auto.
apply FNPredSuc; auto.
apply FcanonicBound with (radix := radix); auto.
Qed.

Theorem FNSucPred :
  x : float,
 Fbounded b x FNSucc b radix precision (FNPred x) = x :>R.
intros x H'; unfold FNSucc in |- *; rewrite FcanonicFnormalizeEq; auto.
unfold FNPred in |- *; rewrite FSucPred; auto.
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
apply FnormalizeCanonic; auto.
apply FNPredCanonic; auto.
Qed.

Theorem FNSucPredEq :
  x : float,
 Fcanonic radix b x FNSucc b radix precision (FNPred x) = x.
intros x H'.
apply FcanonicUnique with (5 := H') (precision := precision); auto.
apply FNSuccCanonic; auto.
apply FcanonicBound with (radix := radix); auto.
apply FNPredCanonic; auto.
apply FcanonicBound with (radix := radix); auto.
apply FNSucPred; auto.
apply FcanonicBound with (radix := radix); auto.
Qed.

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