(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require Reals.Rbasic_fun.
Require Reals.R_sqrt.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.RealInfix.
Require real.Abs.
Require real.FromInt.
Require real.Truncate.
Require real.Square.
Require bv.Pow2int.
Require ieee_float.RoundingMode.

Require Import Flocq.Core.Fcore.
Require Import Flocq.Appli.Fappli_IEEE.
Require Import Flocq.Calc.Fcalc_bracket.
Require Import Flocq.Calc.Fcalc_round.
Require Import Flocq.Prop.Fprop_plus_error.
Require Import ZArith.
Require Import Fourier.
Import real.Truncate.
Import ieee_float.RoundingMode.

(* extra arguments _ below are needed for Coq prior to 8.6
   keep them until support for Coq 8.5 is dropped *)

Arguments B754_zero {prec} {emax} _ .
Arguments B754_infinity {prec} {emax} _.
Arguments B754_nan {prec} {emax} _ _ .
Arguments B754_finite {prec} {emax} _ _ _ _ .

Definition mode_to_IEEE : mode -> Fappli_IEEE.mode.
  exact (fun m =>
           match m with
           | RNE => mode_NE
           | RNA => mode_NA
           | RTP => mode_UP
           | RTN => mode_DN
           | RTZ => mode_ZR
           end).
Defined.

Coercion mode_to_IEEE : mode >-> Fappli_IEEE.mode.

Section GenericFloat.

Variable eb_pos sb_pos : positive.

(* Why3 goal *)
Definition eb: Z.
Proof.
  exact (Z.pos eb_pos).
Defined.

(* Why3 goal *)
Definition sb: Z.
Proof.
  exact (Z.pos sb_pos).
Defined.

Hypothesis Heb : Zlt_bool 1 eb = true.
Hypothesis Hsbb : Zlt_bool 1 sb = true.

(* Why3 goal *)
Lemma eb_gt_1 : (1%Z < eb)%Z.
Proof.
  rewrite Zlt_is_lt_bool.
  apply Heb.
Qed.

(* Why3 goal *)
Lemma sb_gt_1 : (1%Z < sb)%Z.
Proof.
  rewrite Zlt_is_lt_bool.
  apply Hsbb.
Qed.

(* power of infinities *)
Definition emax : Z.
Proof.
  exact (radix2 ^ (eb - 1))%Z.
Defined.

(* Why3 goal *)
Definition t : Type.
Proof.
  exact (binary_float sb emax).
Defined.

(* Why3 goal *)
Definition zeroF: t.
Proof.
  exact (B754_zero false).
Defined.

Definition emin := (3 - emax - sb)%Z.
Notation fexp := (FLT_exp emin sb).

Lemma Hsb : Zlt_bool 0 sb = true.
Proof.
  auto with zarith.
Qed.

Lemma Hsb': (0 < sb)%Z.
Proof.
  unfold sb; auto with zarith.
Qed.

Hypothesis Hemax : Zlt_bool sb emax = true.

Lemma Hemax': (sb < emax)%Z.
Proof.
  rewrite Zlt_is_lt_bool.
  apply Hemax.
Qed.

Instance Hsb'' : Prec_gt_0 sb := Hsb'.

Lemma fexp_Valid : Valid_exp fexp.
Proof.
  apply (fexp_correct _ _ Hsb'').
Qed.

Definition r_to_fp rnd x : binary_float sb emax :=
  let r := round radix2 fexp (round_mode rnd) x in
  let m := Ztrunc (scaled_mantissa radix2 fexp r) in
  let e := canonic_exp radix2 fexp r in
  binary_normalize sb emax Hsb' Hemax' rnd m e false.

Theorem r_to_fp_correct :
  forall rnd x,
  let r := round radix2 fexp (round_mode rnd) x in
  (Rabs r < bpow radix2 emax)%R ->
  is_finite sb emax (r_to_fp rnd x) = true /\
  B2R sb emax (r_to_fp rnd x) = r.
Proof with auto with typeclass_instances.
intros rnd x r Bx.
unfold r_to_fp. fold r.
generalize (binary_normalize_correct sb emax Hsb' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (canonic_exp radix2 fexp r) false).
unfold r.
elim generic_format_round...
fold emin r.
rewrite round_generic...
rewrite Rlt_bool_true with (1 := Bx).
now split.
apply generic_format_round...
Qed.

Theorem r_to_fp_format :
  forall rnd x,
  FLT_format radix2 emin sb x ->
  (Rabs x < bpow radix2 emax)%R ->
  B2R sb emax (r_to_fp rnd x) = x.
Proof with auto with typeclass_instances.
intros rnd x Fx Bx.
assert (Gx: generic_format radix2 fexp x).
apply generic_format_FLT.
apply Fx.
pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (2 := Gx)...
refine (proj2 (r_to_fp_correct _ _ _)).
rewrite round_generic...
Qed.

Lemma max_eb_bounded : bounded sb emax (2 ^ sb_pos - 1) (emax - sb) = true.
Proof.
  assert (0 <= sb - 1)%Z.
  apply Zlt_0_le_0_pred, Hsb'.
  unfold bounded; apply Bool.andb_true_iff; split.
  unfold canonic_mantissa, FLT_exp.
  apply Zeq_bool_true.
  rewrite Fcore_digits.Zpos_digits2_pos.
  rewrite (Fcore_digits.Zdigits_unique radix2 _ sb).
  assert (sb + (emax - sb) - sb = emax - sb)%Z by omega; rewrite H0.
  apply Zmax_left.
  assert (1 < emax)%Z.
  apply Z.le_lt_trans with (m := sb).
  change (Z.succ 0 <= sb)%Z; apply Zgt_le_succ; easy.
  apply Hemax'.
  auto with zarith.
  rewrite Z.abs_eq by auto with zarith.
  change ((2 ^ (sb - 1) <= Z.pos (2 ^ sb_pos - 1) < 2 ^ sb)%Z).
  assert (Z.pos (2 ^ sb_pos - 1) = 2 ^ sb -1)%Z.
  rewrite Pos2Z.inj_sub, Pos2Z.inj_pow.
  fold sb; reflexivity.
  apply Pos.pow_gt_1; easy.
  rewrite H0.
  split; auto with zarith.
  assert (sb = Z.succ (sb - 1)) by auto with zarith.
  rewrite H1 at 2.
  rewrite Z.pow_succ_r by trivial.
  assert (1 <= 2 ^ (sb - 1))%Z.
  apply Z.lt_pred_le, (Zpower_gt_0 radix2 (sb - 1)); trivial.
  omega.
  apply Zle_bool_true; auto with zarith.
Qed.

Definition max_value: t.
Proof.
  exact (B754_finite false (2 ^ sb_pos - 1) (emax - sb) max_eb_bounded).
Defined.

Definition One_Nan_pl: nan_pl sb.
Proof.
  unfold nan_pl, Fcore_digits.digits2_pos.
  exists 1%positive.
  apply Hsbb.
Qed.

Definition One_Nan: t := B754_nan false One_Nan_pl.

Definition nan_bf: binary_float sb emax -> binary_float sb emax -> bool * nan_pl sb.
Proof.
  exact (fun b nan => (true,One_Nan_pl)).
Qed.

(* Why3 goal *)
Definition add: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  exact (Bplus sb emax _ Hemax' nan_bf).
Defined.

(* Why3 goal *)
Definition sub: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  exact (Bminus sb emax _ Hemax' nan_bf).
Defined.

(* Why3 goal *)
Definition mul: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  exact (Bmult sb emax _ Hemax' nan_bf).
Defined.

(* Why3 goal *)
Definition div: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  exact (Bdiv sb emax _ Hemax' nan_bf).
Defined.

(* Why3 goal *)
Definition abs: t -> t.
Proof.
  exact (Babs sb emax pair).
Defined.

(* Why3 goal *)
Definition neg: t -> t.
Proof.
  exact (Bopp sb emax pair).
Defined.

(* Why3 goal *)
Definition fma: ieee_float.RoundingMode.mode -> t -> t -> t -> t.
Admitted.

(* Why3 goal *)
Definition sqrt: ieee_float.RoundingMode.mode -> t -> t.
Proof.
  exact (Bsqrt sb emax Hsb' Hemax' (fun b => (true,One_Nan_pl))).
Defined.

Definition z_to_fp m x := binary_normalize sb emax Hsb' Hemax' (mode_to_IEEE m) x 0 false.

Definition fp_to_z: mode -> t -> Z.
Proof.
  exact (fun m x => match m with
         | RNA => ZnearestA (B2R sb emax x)
         | RNE => ZnearestE (B2R sb emax x)
         | RTP => Zceil (B2R sb emax x)
         | RTN => Zfloor (B2R sb emax x)
         | RTZ => Ztrunc (B2R sb emax x)
         end).
Defined.

(* Why3 goal *)
Definition roundToIntegral: ieee_float.RoundingMode.mode -> t -> t.
Proof.
  exact (fun m x =>
           match x with
             | B754_zero b => B754_zero b
             | B754_infinity b => B754_infinity b
             | B754_nan b n => B754_nan b n
             | B754_finite b ma e _ =>
               let x_int := fp_to_z m x in
               match Z.eq_dec x_int 0%Z with
               | left _ => B754_zero b
               | right _ => z_to_fp RTZ x_int
               end
           end).
Defined.

(* Why3 goal *)
Definition min: t -> t -> t.
Proof.
  exact (fun x y => match Bcompare _ _ x y with
           | Some Lt => x
           | Some Gt | Some Eq => y
           | None => One_Nan
         end).
Defined.

(* Why3 goal *)
Definition max: t -> t -> t.
Proof.
  exact (fun x y => match Bcompare _ _ x y with
           | Some Lt => y
           | Some Gt | Some Eq => x
           | None => One_Nan
         end).
Defined.

(* Why3 goal *)
Definition le: t -> t -> Prop.
Proof.
  exact (fun a b => Bcompare _ _ a b = Some Lt \/ Bcompare _ _ a b = Some Eq).
Defined.

Hint Unfold le.

(* Why3 goal *)
Definition lt: t -> t -> Prop.
Proof.
  exact (fun a b => Bcompare _ _ a b = Some Lt).
Defined.

Hint Unfold lt.

Lemma gt_bcompare : forall {x y}, lt y x <-> Bcompare _ _ x y = Some Gt.
Proof.
  intros x y.
  rewrite Bcompare_swap.
  unfold lt.
  destruct Bcompare.
  destruct c; simpl; split; intro h; inversion h; auto.
  split; intro h; inversion h; auto.
Qed.

Lemma ge_bcompare : forall {x y}, le y x <-> Bcompare _ _ x y = Some Gt \/ Bcompare _ _ x y = Some Eq.
Proof.
  intros x y.
  unfold le.
  rewrite <-gt_bcompare.
  assert (Bcompare _ _ y x = Some Eq <-> Bcompare _ _ x y = Some Eq).
  rewrite Bcompare_swap.
  destruct Bcompare; try (split; now auto).
  destruct c; simpl; split; intro h; inversion h; auto.
  rewrite H; reflexivity.
Qed.

(* Why3 goal *)
Definition eq: t -> t -> Prop.
Proof.
  exact (fun a b => Bcompare _ _ a b = Some Eq).
Defined.

Hint Unfold eq.

Lemma le_correct: forall x y, le x y <-> lt x y \/ eq x y.
Proof.
  intros x y; split; intro h; destruct h; auto.
Qed.

Lemma lt_le: forall {x y}, lt x y -> le x y.
Proof.
  intros x y.
  rewrite le_correct; auto.
Qed.

Lemma eq_zero_iff: forall {x}, eq zeroF x <-> x = zeroF \/ x = neg zeroF.
Proof.
  intro; unfold eq; destruct x ; destruct b; simpl.
  split; auto.
  split; auto.
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
Qed.

(* Why3 goal *)
Definition is_normal: t -> Prop.
Proof.
  exact (fun x => match x with
                    | B754_zero _ => True
                    | B754_finite _ _ e _ => (emin < e)%Z
                    | _ => False
        end).
Defined.

(* Why3 goal *)
Definition is_subnormal: t -> Prop.
Proof.
  exact (fun x => match x with
                    | B754_finite _ _ e _ => (emin = e)%Z
                    | _ => False
        end).
Defined.

(* Why3 goal *)
Definition is_zero: t -> Prop.
Proof.
  exact (fun x => eq zeroF x).
Defined.

Lemma zero_is_zero: forall {b}, is_zero (B754_zero b).
Proof.
  easy.
Qed.

Lemma is_zero_B754_zero :
  forall x, is_zero x <-> exists b, x = B754_zero b.
Proof.
  intro.
  unfold is_zero; rewrite eq_zero_iff.
  unfold zeroF.
  simpl neg.
  split; intro h; destruct h; auto; try easy.
  exists false; assumption.
  exists true; assumption.
  destruct x0;[right|left];auto.
Qed.

Lemma zero_or_not : forall x, ~ is_zero x \/ is_zero x.
Proof.
  destruct x ; destruct b; try (right; easy); left; simpl; try easy.
Qed.

(* Why3 goal *)
Definition is_infinite: t -> Prop.
Proof.
  exact (fun x => match x with
                  | B754_infinity _ => True
                  | _ => False
                  end).
Defined.

Coercion is_true : bool >-> Sortclass.

Lemma eq_infinite_dist: forall {x y}, eq x y -> is_infinite x -> is_infinite y.
Proof.
  intros; destruct x, y; try easy; destruct b,b0; easy.
Qed.

(* Why3 goal *)
Definition is_nan: t -> Prop.
Proof.
  exact (is_nan sb emax).
Defined.

Lemma is_infinite_not_nan: forall {x}, is_infinite x -> ~ is_nan x.
Proof.
  intro x; destruct x; easy.
Qed.

Lemma le_infinity: forall {x}, ~ is_nan x -> le x (B754_infinity false).
Proof.
  intros.
  unfold le.
  destruct x; try easy.
  + left; easy.
  + destruct b; unfold Bcompare; [left|right]; easy.
  + contradict H; easy.
  + destruct b; left; easy.
Qed.

Lemma is_nan_dec: forall x, {is_nan x} + {~ is_nan x}.
Proof.
  intro; destruct x; compute; intuition.
Qed.

Lemma eq_not_nan_refl: forall {x : t}, ~ is_nan x -> eq x x.
Proof.
  intros; destruct x; auto.
  destruct b; auto.
  destruct H; easy.
  destruct b; unfold eq; simpl; rewrite Z.compare_refl, Pcompare_refl; easy.
Qed.

Lemma eq_not_nan: forall {x y}, eq x y -> ~ is_nan x /\ ~ is_nan y.
Proof.
  intros; destruct x; destruct y; try easy; intuition; destruct b; easy.
Qed.

Lemma lt_not_nan: forall {x y}, lt x y -> ~ is_nan x /\ ~ is_nan y.
Proof.
  intros; destruct x, y; try easy; intuition; destruct b; easy.
Qed.

Lemma le_or_lt_or_nan: forall x y, le x y \/ lt y x \/ is_nan x \/ is_nan y.
Proof.
  unfold is_nan.
  destruct x, y; auto; try easy;
    try (destruct b, b0; auto; easy).
  unfold le, lt.
  set (x:=(B754_finite b m e e0)).
  set (y:=(B754_finite b0 m0 e1 e2)).
  rewrite (Bcompare_correct sb emax x y), (Bcompare_correct sb emax y x); auto.
  destruct (Rtotal_order (B2R sb emax x) (B2R sb emax y)) as [h|[h|h]].
  rewrite (Rcompare_Lt _ _ h), (Rcompare_Gt _ _ h); auto.
  rewrite Rcompare_Eq; auto.
  rewrite (Rcompare_Lt _ _ (Rfourier_gt_to_lt _ _  h)), (Rcompare_Gt _ _ (Rfourier_gt_to_lt _ _ h)); auto.
Qed.

(* Why3 goal *)
Definition is_positive: t -> Prop.
Proof.
  exact (fun x => match x with
                    | B754_zero false => True
                    | B754_finite false _ e _ => True
                    | B754_infinity false => True
                    | _ => False
        end).
Defined.

Hint Unfold is_positive.

Lemma is_positive_Bsign: forall x, ~ is_nan x -> (is_positive x <-> Bsign sb emax x = false).
Proof.
  split.
  destruct x ; destruct b; try easy.
  destruct x ; destruct b; try easy.
  contradict H; easy.
Qed.

Lemma is_positive_correct: forall x, is_positive x <-> lt zeroF x \/ x = B754_zero false.
Proof.
  split.
  intro h; destruct x ; destruct b; auto; easy.
  intro h; destruct h; destruct x ; destruct b; easy.
Qed.

(* Why3 goal *)
Definition is_negative: t -> Prop.
Proof.
  exact (fun x => match x with
                    | B754_zero true => True
                    | B754_finite true _ e _ => True
                    | B754_infinity true => True
                    | _ => False
        end).
Defined.

Hint Unfold is_negative.

Lemma is_negative_Bsign: forall x, ~ is_nan x -> (is_negative x <-> Bsign sb emax x = true).
Proof.
  split.
  destruct x ; destruct b; easy.
  destruct x ; destruct b; easy.
Qed.

Lemma is_negative_correct: forall x, is_negative x <-> lt x zeroF \/ x = B754_zero true.
Proof.
  split.
  intro h; destruct x ; destruct b; auto; easy.
  intro h; destruct h; destruct x ; destruct b; easy.
Qed.

(* Why3 goal *)
Definition is_finite: t -> Prop.
  exact (is_finite sb emax).
Defined.

Lemma not_nan: forall x, ~ (is_nan x) -> {is_finite x} + {is_infinite x}.
Proof.
  unfold is_nan, is_finite.
  intro x; destruct x; simpl; intro; auto.
Qed.

Lemma is_finite_not_nan: forall {x}, is_finite x -> ~ is_nan x.
Proof.
  intro x; destruct x; easy.
Qed.

Lemma Finite_Infinite_Nan_dec: forall x:t, {is_finite x} + {is_infinite x} + {is_nan x}.
Proof.
  intro x; destruct x; simpl.
  left; left; easy.
  left; right; easy.
  right; easy.
  left; left; easy.
Qed.

Lemma eq_finite_dist: forall {x y}, eq x y -> is_finite x -> is_finite y.
Proof.
  intros; destruct x, y; try easy; destruct b,b0; easy.
Qed.

Lemma bounded_floats :
  forall x:t, (is_finite x) ->
              Bcompare sb emax (abs x) max_value = Some Lt
           \/ Bcompare sb emax (abs x) max_value = Some Eq.
Proof.
  destruct x; try easy; auto; (* simpl; *) intros.
  destruct (andb_prop _ _ e0) as (H1,H2).
  generalize (Zeq_bool_eq _ _ H1); clear H1; intro H1.
  generalize (Zle_bool_imp_le _ _ H2); clear H2; intro H2.
  destruct (Z_le_lt_eq_dec _ _ H2); clear H2.
  simpl; rewrite (Zcompare_Lt _ _ l); auto.
  simpl; rewrite (Zcompare_Eq _ _ e1).
  unfold FLT_exp in H1.
  rewrite Fcore_digits.Zpos_digits2_pos in H1.
  assert (3 - emax - sb <= Fcore_digits.Zdigits radix2 (Z.pos m) + e - sb)%Z.
  rewrite e1.
  pose sb_gt_1. pose Hemax'.
  assert (Z.pos m <> 0)%Z. pose (Pos2Z.is_pos m); auto with zarith.
  pose (Fcore_digits.Zdigits_gt_0 radix2 (Z.pos m) H0).
  auto with zarith.
  rewrite <-Z.max_l_iff in H0.
  rewrite H0 in H1; clear H0.
  assert (Fcore_digits.Zdigits radix2 (Z.pos m) = sb) by auto with zarith; clear H1.
  pose (Fcore_digits.Zdigits_correct radix2 (Z.pos m)).
  rewrite H0 in a.
  replace (Z.abs (Z.pos m)) with (Z.pos m) in a by auto with zarith.
  destruct a. clear H1.
  assert (Z.pos m = radix2 ^ sb - 1 \/ Z.pos m < radix2 ^ sb - 1)%Z by omega.
  destruct H1.
  right.
  replace (radix2 ^ sb)%Z with (Z.pos 2 ^ Z.pos sb_pos)%Z in H1 by auto.
  rewrite <-Pos2Z.inj_pow, <-Pos2Z.inj_sub, <-Zpos_eq_iff in H1.
  rewrite H1.
  rewrite Pcompare_refl; reflexivity.
  apply Pos.pow_gt_1; easy.
  left.
  rewrite nat_of_P_lt_Lt_compare_complement_morphism. reflexivity.
  apply Pos2Nat.inj_lt.
  replace (radix2 ^ sb)%Z with (Z.pos 2 ^ Z.pos sb_pos)%Z in H1 by auto.
  rewrite <-Pos2Z.inj_pow, <-Pos2Z.inj_sub in H1.
  auto with zarith.
  apply Pos.pow_gt_1; easy.
Qed.

Lemma bounded_floats_le: forall x, is_finite x -> le (abs x) max_value.
Proof.
  apply bounded_floats.
Qed.

Lemma is_finite_B: forall (x:t),
    is_finite x ->
    exists b, x = B754_zero b \/ exists b m e p, x = B754_finite b m e p.
Proof.
  intro x.
  destruct x; try easy; intros.
  exists b; auto.
  exists b; right.
  exists b, m, e, e0; trivial.
Qed.

(* Why3 assumption *)
Definition is_plus_infinity (x:t): Prop := (is_infinite x) /\ (is_positive
  x).

(* Why3 assumption *)
Definition is_minus_infinity (x:t): Prop := (is_infinite x) /\ (is_negative
  x).

(* Why3 assumption *)
Definition is_plus_zero (x:t): Prop := (is_zero x) /\ (is_positive x).

(* Why3 assumption *)
Definition is_minus_zero (x:t): Prop := (is_zero x) /\ (is_negative x).

(* Why3 assumption *)
Definition is_not_nan (x:t): Prop := (is_finite x) \/ (is_infinite x).

(* Why3 goal *)
Lemma is_not_nan1 : forall (x:t), (is_not_nan x) <-> ~ (is_nan x).
Proof.
  unfold is_not_nan; split; intro H.
  destruct H; [apply is_finite_not_nan|apply is_infinite_not_nan];trivial.
  destruct (not_nan _ H); auto.
Qed.

(* Why3 goal *)
Lemma is_not_finite : forall (x:t), (~ (is_finite x)) <-> ((is_infinite x) \/
  (is_nan x)).
Proof.
intros x.
destruct x; split; intro h; try easy.
contradict h; easy.
destruct h as [h|h]; contradict h; easy.
left; easy.
right; easy.
contradict h; easy.
destruct h as [h|h]; contradict h; easy.
Qed.

(* Why3 goal *)
Definition to_real: t -> R.
Proof.
  exact (B2R sb emax).
Defined.

Lemma Some_ext: forall {T} (a b:T), Some a = Some b <-> a = b.
Proof.
  intros; split; intro H;[inversion H|rewrite H]; reflexivity.
Qed.

Lemma to_real_eq: forall {x:t} {y:t}, is_finite x -> is_finite y ->
                                      (eq x y <-> to_real x = to_real y).
Proof.
  intros x y h1 h2.
  unfold eq.
  rewrite (Bcompare_correct _ _ x y h1 h2), Some_ext.
  split; intro H; [apply (Rcompare_Eq_inv _ _ H)|
                   apply (Rcompare_Eq _ _ H)].
Qed.

Lemma to_real_eq_alt: forall {x y}, eq x y -> to_real x = to_real y.
Proof.
  destruct x, y; destruct b, b0; unfold eq, Bcompare; try easy.
  - destruct (Z_dec e e1) as [[s|s]|s].
    + rewrite Zcompare_Lt by auto; intro; easy.
    + apply Z.gt_lt in s.
      rewrite Zcompare_Gt by auto; intro; easy.
    + rewrite Zcompare_Eq by auto; intro.
      inversion H.
      rewrite <-ZC4 in H1.
      apply Pcompare_Eq_eq in H1.
      destruct m; simpl; subst; auto.
  - destruct (Z_dec e e1) as [[s|s]|s].
    + rewrite Zcompare_Lt by auto; intro; easy.
    + apply Z.gt_lt in s.
      rewrite Zcompare_Gt by auto; intro; easy.
    + rewrite Zcompare_Eq by auto; intro.
      inversion H.
      apply Pcompare_Eq_eq in H1.
      destruct m; simpl; subst; auto.
Qed.

Lemma le_to_real: forall (x:t) (y:t), is_finite x -> is_finite y ->
  (le x y <-> (to_real x <= to_real y)).
Proof.
intros x y h1 h2.
unfold le.
rewrite (Bcompare_correct _ _ x y h1 h2), Some_ext, Some_ext.
split; intro H.
destruct H; [apply Rlt_le; apply (Rcompare_Lt_inv _ _ H)|
             apply Req_le; apply (Rcompare_Eq_inv _ _ H)].
destruct H; [left; apply (Rcompare_Lt _ _ H)|
             right; apply (Rcompare_Eq _ _ H)].
Qed.

(* Why3 goal *)
Lemma zeroF_is_positive : (is_positive zeroF).
Proof.
easy.
Qed.

(* Why3 goal *)
Lemma zeroF_is_zero : (is_zero zeroF).
Proof.
  apply eq_refl; easy.
Qed.

Lemma zeroF_to_real : ((to_real zeroF) = 0%R).
Proof.
easy.
Qed.

Lemma B754_zero_to_real: forall {b}, to_real (B754_zero b) = 0.
Proof.
  intro b.
  rewrite <-(to_real_eq_alt zero_is_zero).
  apply zeroF_to_real.
Qed.

(* Why3 goal *)
Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((is_finite x) /\
  ((to_real x) = 0%R)).
Proof.
  unfold is_zero.
  assert (is_finite zeroF) by easy.
  intros x; split; intro H0.
  assert (is_finite x) by apply (eq_finite_dist H0 H).
  split; auto.
  symmetry.
  rewrite <-(to_real_eq H H1); auto.
  destruct H0.
  rewrite to_real_eq; auto.
Qed.

(* Why3 goal *)
Notation of_int := z_to_fp.

(* Why3 goal *)
Notation to_int := fp_to_z.

Lemma to_int_zeroF: forall m, to_int m zeroF = 0%Z.
Proof.
  intro m.
  destruct (valid_rnd_round_mode m) as (_,b).
  pose proof (b 0%Z) as H; simpl in H.
  destruct m; simpl; auto.
Qed.

(* add to theory ? *)
Lemma to_int_eq: forall {m x y}, eq x y -> to_int m x = to_int m y.
Proof.
  destruct x, y; destruct b, b0; unfold eq, Bcompare; try easy.
  - destruct (Z_dec e e1) as [[s|s]|s].
    + rewrite Zcompare_Lt by auto; intro; easy.
    + apply Z.gt_lt in s.
      rewrite Zcompare_Gt by auto; intro; easy.
    + rewrite Zcompare_Eq by auto; intro.
      inversion H.
      rewrite <-ZC4 in H1.
      apply Pcompare_Eq_eq in H1.
      destruct m; simpl; subst; auto.
  - destruct (Z_dec e e1) as [[s|s]|s].
    + rewrite Zcompare_Lt by auto; intro; easy.
    + apply Z.gt_lt in s.
      rewrite Zcompare_Gt by auto; intro; easy.
    + rewrite Zcompare_Eq by auto; intro.
      inversion H.
      apply Pcompare_Eq_eq in H1.
      destruct m; simpl; subst; auto.
Qed.

Lemma to_int_B754_zero: forall {b m}, to_int m (B754_zero b) = 0%Z.
Proof.
  intros b m.
  rewrite <-(to_int_eq zero_is_zero).
  apply to_int_zeroF.
Qed.

(* add to theory ? *)
Lemma to_int_le: forall {x y m}, is_finite x -> is_finite y -> le x y -> (to_int m x <= to_int m y)%Z.
Proof.
  intros.
  destruct m;

  [destruct (valid_rnd_round_mode mode_NE)|
   destruct (valid_rnd_NA)|
   destruct (valid_rnd_UP)|
   destruct (valid_rnd_DN)|
   destruct (valid_rnd_ZR)];
  apply Zrnd_le;
  apply le_to_real; auto.
Qed.

(* Why3 goal *)
Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode),
  (zeroF = (of_int m 0%Z)).
Proof.
auto.
Qed.

(* Why3 goal *)
Definition round: ieee_float.RoundingMode.mode -> R -> R.
Proof.
  exact (fun m => round radix2 fexp (round_mode m)).
Defined.

(* Why3 goal *)
Definition max_real: R.
Proof.
  exact ((1 - bpow radix2 (- sb)) * bpow radix2 emax).
Defined.

Lemma max_real_is_F2R: @F2R radix2 {| Fnum := Z.pos (2 ^ sb_pos - 1); Fexp := emax - sb |} = max_real.
Proof.
  unfold F2R.
  unfold Fnum, Fexp.
  rewrite Pos2Z.inj_sub, Pos2Z.inj_pow, Z2R_minus.
  fold sb.
  simpl (Z2R 1).
  change 2%Z with (radix_val radix2).
  rewrite Z2R_Zpower by easy.
  rewrite Int.infix_mn_def, bpow_plus.
  rewrite Rmult_comm, Rmult_assoc, Rmult_comm, Rmult_minus_distr_l.
  rewrite <-bpow_plus.
  replace (- sb + sb)%Z with 0%Z by auto with zarith.
  replace (bpow radix2 0) with 1 by auto.
  rewrite Rmult_1_r.
  reflexivity.
  apply Pos.pow_gt_1; easy.
Qed.

Lemma min_real_is_F2R: @F2R radix2 {| Fnum := Z.neg (2 ^ sb_pos - 1); Fexp := emax - sb |} = - max_real.
Proof.
  rewrite <-max_real_is_F2R.
  rewrite <-Fcalc_ops.F2R_opp.
  unfold Fcalc_ops.Fopp.
  reflexivity.
Qed.

Lemma max_value_to_real: to_real max_value = max_real.
Proof.
  unfold B2R; simpl.
  apply max_real_is_F2R.
Qed.

Lemma max_real_alt : max_real = bpow radix2 emax - bpow radix2 (emax - sb).
Proof.
  unfold max_real.
  rewrite Rmult_minus_distr_r, Rmult_1_l.
  rewrite <-bpow_plus.
  replace (- sb + emax)%Z with (emax - sb)%Z by auto with zarith.
  reflexivity.
Qed.

Lemma max_real_lt_bpow_radix2_emax: max_real < bpow radix2 emax.
Proof.
  rewrite max_real_alt.
  assert (0 < bpow radix2 (emax - sb)) by apply bpow_gt_0.
  fourier.
Qed.

Lemma max_real_ge_6: 6 <= max_real.
Proof.
  rewrite max_real_alt.
  assert (2 <= sb)%Z by (pose proof sb_gt_1; auto with zarith).
  assert (sb + 1 <= emax)%Z by (pose proof Hemax'; auto with zarith).
  assert (3 <= emax)%Z by auto with zarith.
  assert (8 <= bpow radix2 emax).
  assert (8 = bpow radix2 3) by easy.
  rewrite H2.
  apply bpow_le; assumption.
  change (6 <= bpow radix2 emax - bpow radix2 (emax + (- sb))).
  rewrite bpow_plus.
  assert (bpow radix2 (- sb) <= /4).
  assert (/4 = bpow radix2 (-2)) by easy.
  rewrite H3.
  apply bpow_le.
  rewrite <-(Z.opp_le_mono 2 sb); assumption.
  assert (bpow radix2 emax * bpow radix2 (-sb) <= bpow radix2 emax * / 4).
  apply Rfourier_le; auto; fourier.
  fourier.
Qed.

Lemma max_real_generic_format: generic_format radix2 fexp max_real.
Proof.
  rewrite <-max_value_to_real.
  apply generic_format_B2R.
Qed.

(* Why3 goal *)
Definition max_int: Z.
Proof.
  exact (2 ^ emax - 2 ^ (emax - sb))%Z.
Defined.

(* Why3 goal *)
Lemma max_int1 : (max_int = ((bv.Pow2int.pow2 (bv.Pow2int.pow2 (eb - 1%Z)%Z)) - (bv.Pow2int.pow2 ((bv.Pow2int.pow2 (eb - 1%Z)%Z) - sb)%Z))%Z).
Proof.
  rewrite two_p_equiv, two_p_equiv, two_p_equiv.
  now unfold max_int, emax.
Qed.

(* Why3 goal *)
Lemma max_real_int : (max_real = (BuiltIn.IZR max_int)).
Proof.
  unfold max_int.
  rewrite <-Z2R_IZR, Z2R_minus.
  change 2%Z with (radix_val radix2).
  rewrite Z2R_Zpower, Z2R_Zpower by (pose Hsb'; pose Hemax'; auto with zarith).
  apply max_real_alt.
Qed.

(* Why3 assumption *)
Definition in_range (x:R): Prop := ((-max_real)%R <= x)%R /\
  (x <= max_real)%R.

(* Why3 assumption *)
Definition in_int_range (i:Z): Prop := ((-max_int)%Z <= i)%Z /\
  (i <= max_int)%Z.

Lemma in_range_bpow_radix2_emax: forall x, in_range x -> Rabs x < bpow radix2 emax.
Proof.
  unfold in_range; intros.
  apply Rle_lt_trans with (r2:= max_real).
  apply Abs.Abs_le; apply H.
  apply max_real_lt_bpow_radix2_emax.
Qed.

Lemma is_finite_abs : forall x:t, is_finite x -> is_finite (abs x).
Proof.
  destruct x; try easy.
Qed.

(* Why3 goal *)
Lemma is_finite1 : forall (x:t), (is_finite x) -> (in_range (to_real x)).
Proof.
  intros x h1.
  apply Rabs_le_inv.
  rewrite <-max_value_to_real.
  apply Rcompare_not_Lt_inv.
  pose (is_finite_abs x h1).
  pose (bounded_floats x h1).
  rewrite Bcompare_correct in o; try easy.
  unfold abs in o.
  rewrite B2R_Babs in o.
  unfold to_real.
  intro H0.
  destruct o as [H|H]; inversion H as (H1);
  rewrite Rcompare_sym in H1; apply CompOpp_iff in H1;
  simpl in H0; rewrite H0 in H1;
  inversion H1.
Qed.

Lemma Rabs_round_max_real_emax:
  forall {m} {x}, Rabs (round m x) <= max_real <-> Rabs (round m x) < bpow radix2 emax.
Proof.
  intros m x; split; intro h.
  - apply Rle_lt_trans with (r2 := max_real).
    apply h.
    apply max_real_lt_bpow_radix2_emax.
  - destruct (r_to_fp_correct m x h).
    unfold round.
    rewrite <-H0, Abs.Abs_le.
    apply (is_finite1 _ H).
Qed.

(* Why3 assumption *)
Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R): Prop :=
  (in_range (round m x)).

Lemma no_overflow_Rabs_round_max_real: forall {m} {x}, no_overflow m x <-> Rabs (round m x) <= max_real.
Proof.
  intro x.
  split; intro h; apply Abs.Abs_le; easy.
Qed.

Lemma no_overflow_Rabs_round_emax: forall {m} {x}, no_overflow m x <-> Rabs (round m x) < bpow radix2 emax.
Proof.
  intros m x.
  apply (iff_trans no_overflow_Rabs_round_max_real Rabs_round_max_real_emax).
Qed.

Lemma IZR_alt: forall {x}, @F2R radix2 {| Fnum := x; Fexp := 0 |} = IZR x.
Proof.
  intros; unfold F2R, Fnum, Fexp, FLT_exp.
  assert (bpow radix2 0 = 1) as bpow_0 by easy.
  rewrite bpow_0, Rmult_1_r, Z2R_IZR.
  reflexivity.
Qed.

Lemma of_int_correct :
  forall {m} {x},
    no_overflow m (IZR x) ->
      to_real (of_int m x) = round m (IZR x) /\ is_finite (of_int m x) /\
      Bsign sb emax (of_int m x) =
      match (x ?= 0)%Z with
      | Eq => false
      | Lt => true
      | Gt => false
      end.
Proof.
  intros m x h1.
  generalize (binary_normalize_correct sb emax Hsb' Hemax' m x 0 false).
  rewrite Rlt_bool_true.
  - intro; destruct H; destruct H0.
    rewrite IZR_alt in H1.
    split.
    rewrite IZR_alt in H; auto.
    split; auto.
    rewrite <-Rcompare_Z2R.
    rewrite Z2R_IZR; auto.

  - apply no_overflow_Rabs_round_emax.
    rewrite IZR_alt; apply h1.
Qed.

(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:ieee_float.RoundingMode.mode)
  (x:R), (in_range x) -> (no_overflow m x).
Proof.
intros m x h1.
rewrite no_overflow_Rabs_round_max_real.
apply abs_round_le_generic.
apply fexp_Valid.
apply valid_rnd_round_mode.
apply max_real_generic_format.
rewrite Abs.Abs_le; easy.
Qed.

(* Why3 goal *)
Lemma Round_monotonic : forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R),
  (x <= y)%R -> ((round m x) <= (round m y))%R.
Proof.
  intros m x y h1.
  apply round_le.
  apply fexp_Valid.
  apply valid_rnd_round_mode.
  apply h1.
Qed.

Lemma round_lt : forall {x y} {m:mode}, round m x < round m y -> x < y.
Proof.
  intros x y m h.
  case (Rlt_dec x y); auto.
  intro.
  apply Rnot_lt_le in n.
  apply (Round_monotonic m) in n.
  apply RIneq.Rle_not_lt in n.
  contradict h; assumption.
Qed.

(* Why3 goal *)
Lemma Round_idempotent : forall (m1:ieee_float.RoundingMode.mode)
  (m2:ieee_float.RoundingMode.mode) (x:R), ((round m1 (round m2
  x)) = (round m2 x)).
Proof with auto with typeclass_instances.
intros m1 m2 x.
apply round_generic...
apply generic_format_round...
Qed.

(* Why3 goal *)
Lemma Round_to_real : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (is_finite x) -> ((round m (to_real x)) = (to_real x)).
Proof with auto with typeclass_instances.
intros m x h.
apply round_generic...
apply generic_format_B2R.
Qed.

(* Why3 goal *)
Lemma Round_down_le : forall (x:R), ((round ieee_float.RoundingMode.RTN
  x) <= x)%R.
Proof with auto with typeclass_instances.
intros x.
apply round_DN_pt...
Qed.

(* Why3 goal *)
Lemma Round_up_ge : forall (x:R), (x <= (round ieee_float.RoundingMode.RTP
  x))%R.
Proof with auto with typeclass_instances.
intros x.
apply round_UP_pt...
Qed.

(* Why3 goal *)
Lemma Round_down_neg : forall (x:R), ((round ieee_float.RoundingMode.RTN
  (-x)%R) = (-(round ieee_float.RoundingMode.RTP x))%R).
Proof.
intros x.
apply round_opp.
Qed.

(* Why3 goal *)
Lemma Round_up_neg : forall (x:R), ((round ieee_float.RoundingMode.RTP
  (-x)%R) = (-(round ieee_float.RoundingMode.RTN x))%R).
Proof.
intros x.
pattern x at 2 ; rewrite <- Ropp_involutive.
rewrite Round_down_neg.
now rewrite Ropp_involutive.
Qed.

(* Why3 goal *)
Definition pow2sb: Z.
Proof.
  exact (Zpower 2 sb).
Defined.

(* Why3 goal *)
Lemma pow2sb1 : (pow2sb = (bv.Pow2int.pow2 sb)).
Proof.
  now rewrite two_p_equiv.
Qed.

(* Why3 assumption *)
Definition in_safe_int_range (i:Z): Prop := ((-pow2sb)%Z <= i)%Z /\
  (i <= pow2sb)%Z.

Lemma max_rep_int_bounded: bounded sb emax (shift_pos (sb_pos - 1) 1) 1 = true.
Proof.
  unfold bounded.
  apply Bool.andb_true_iff; split.
  unfold canonic_mantissa.
  apply Zeq_bool_true.
  rewrite Fcore_digits.Zpos_digits2_pos, shift_pos_correct.
  rewrite Zmult_1_r, Z.pow_pos_fold.
  rewrite Fcore_digits.Zdigits_Zpower by easy.
  rewrite Pos2Z.inj_sub by exact sb_gt_1.
  fold sb.
  unfold FLT_exp.
  replace (sb - 1 + 1 + 1 - sb)%Z with 1%Z by ring.
  apply Zmax_l.
  pose sb_gt_1; pose Hemax'; omega.
  apply Zle_bool_true.
  pose Hemax'; pose Hsbb; omega.
Qed.

Definition Bmax_rep_int: t.
Proof.
  exact (B754_finite false _ _ max_rep_int_bounded).
Defined.

Lemma IZR_pow2sb: IZR pow2sb = bpow radix2 sb.
Proof.
  unfold pow2sb. simpl.
  rewrite Z2R_IZR; reflexivity.
Qed.

Lemma Bmax_rep_int_to_real: to_real Bmax_rep_int = IZR pow2sb.
Proof.
  rewrite IZR_pow2sb.
  unfold B2R; simpl.
  rewrite shift_pos_correct.
  rewrite Z.pow_pos_fold.
  unfold F2R.
  unfold Fnum, Fexp.
  rewrite Zmult_1_r.
  change 2%Z with (radix_val radix2).
  rewrite Z2R_Zpower by easy.
  rewrite <-bpow_plus.
  rewrite Pos2Z.inj_sub by exact sb_gt_1.
  replace (Z.pos sb_pos - 1 + 1)%Z with (Z.pos sb_pos).
  reflexivity.
  ring.
Qed.

Lemma pow2sb_lt_max_int: (pow2sb <= max_int)%Z.
Proof.
  apply le_IZR.
  rewrite <-max_real_int, <-Bmax_rep_int_to_real.
  now apply is_finite1.
Qed.

Lemma rep_int_in_range:
  forall i, (- pow2sb <= i <= pow2sb)%Z ->
            in_range (IZR i).
Proof.
  intros.
  rewrite <-Z.abs_le in H.
  pose (IZR_le _ _ H).
  rewrite <-Rabs_Zabs in r.
  unfold in_range.
  apply Rabs_le_inv.
  apply Rle_trans with (r2 := IZR pow2sb); auto.

  rewrite <-Bmax_rep_int_to_real, <-max_value_to_real.
  apply le_to_real; try easy.

  assert (is_finite Bmax_rep_int) by easy.
  pose (bounded_floats _ H0).
  rewrite le_correct.
  easy.
Qed.

(* Why3 goal *)
Lemma Exact_rounding_for_integers : forall (m:ieee_float.RoundingMode.mode)
  (i:Z), (in_safe_int_range i) -> ((round m
  (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof with auto with typeclass_instances.
intros m z Hz.
apply round_generic...
assert (Zabs z <= pow2sb)%Z.
apply Z.abs_le with (1:=Hz).
destruct (Zle_lt_or_eq _ _ H) as [Bz|Bz] ; clear H Hz.
apply generic_format_FLT.
exists (Float radix2 z 0).
unfold F2R ; simpl.
split.
rewrite Z2R_IZR.
now rewrite Rmult_1_r.
split. easy.
unfold emin; generalize Hsb' Hemax'; omega.
unfold pow2sb in Bz.
change 2%Z with (radix_val radix2) in Bz.
apply generic_format_abs_inv.
rewrite  <- Z2R_IZR, <- Z2R_abs, Bz, Z2R_Zpower.
apply generic_format_bpow.
unfold FLT_exp, emin.
clear Bz; generalize Hsb' Hemax'; zify.
omega.
apply Zlt_le_weak.
apply Hsb'.
Qed.

Lemma in_safe_int_range_no_overflow : forall m {i}, in_safe_int_range i -> no_overflow m (IZR i).
Proof.
  intros m i h.
  apply Bounded_real_no_overflow.
  unfold in_safe_int_range in h.
  unfold in_range.
  rewrite max_real_int, <-FromInt.Neg, <-Z2R_IZR, <-Z2R_IZR, <-Z2R_IZR.
  pose proof pow2sb_lt_max_int.
  split; apply Z2R_le; auto with zarith.
Qed.

(* Why3 assumption *)
Definition same_sign (x:t) (y:t): Prop := ((is_positive x) /\ (is_positive
  y)) \/ ((is_negative x) /\ (is_negative y)).

Hint Unfold same_sign.

Lemma same_sign_refl: forall {x}, ~ is_nan x -> same_sign x x.
Proof.
  unfold is_nan, same_sign.
  intros x h.
  destruct x; try easy; try (destruct b; now auto).
  now contradict h.
Qed.

(* Why3 assumption *)
Definition diff_sign (x:t) (y:t): Prop := ((is_positive x) /\ (is_negative
  y)) \/ ((is_negative x) /\ (is_positive y)).

Hint Unfold same_sign.

(* Why3 goal *)
Lemma feq_eq : forall (x:t) (y:t), (is_finite x) -> ((is_finite y) ->
  ((~ (is_zero x)) -> ((eq x y) -> (x = y)))).
Proof.
intros x y h1 h2 h3 h4.
destruct x, y; try easy.

destruct b, b0; try easy.
destruct b, b0; try easy.

revert h3 h4.
case (Bool.bool_dec b b0); intro h; [rewrite h;clear h|destruct b, b0; try easy; destruct h;reflexivity].
intros h3 h4. clear h1.

case (Z_dec e e1); intro.

- unfold eq in h4; simpl in h4.
  destruct s.
  rewrite (Zcompare_Lt _ _ l) in h4.
  destruct b, b0; try easy.
  rewrite (Zcompare_Gt _ _ (Z.gt_lt _ _ g)) in h4.
  destruct b, b0; try easy.

- destruct e3.
  case (Pos.eq_dec m m0); intro.
  + destruct e1.
    assert (forall x y: bool, x = y \/ x <> y) by
        (intros; case (Bool.bool_dec x y); auto).
    destruct (Eqdep_dec.eq_proofs_unicity H e0 e2).
    reflexivity.

  + unfold eq in h4; simpl in h4.
    destruct b0.
    * rewrite Z.compare_refl, Some_ext, Pos.compare_cont_antisym in h4.
      rewrite (Pos.compare_eq _ _ h4) in n.
      destruct n; reflexivity.

    * rewrite Z.compare_refl, Some_ext in h4.
      rewrite (Pos.compare_eq _ _ h4) in n.
      destruct n; reflexivity.
Qed.

Lemma to_real_refl: forall {x:t} {y:t}, is_finite x -> is_finite y ->
                                        to_real x = to_real y -> same_sign x y ->
                                        x = y.
Proof.
  intros x y h1 h2 h3 h4.
  destruct x, y; try easy.
  + destruct b, b0, h4; easy.
  + symmetry in h3.
    apply F2R_eq_0_reg in h3.
    destruct b0; contradict h3; easy.
  + apply F2R_eq_0_reg in h3.
    destruct b; contradict h3; easy.
  + apply feq_eq; auto.
    rewrite eq_zero_iff; intro.
    destruct H; easy.
    apply to_real_eq; auto.
Qed.

(* Why3 goal *)
Lemma eq_feq : forall (x:t) (y:t), (is_finite x) -> ((is_finite y) ->
  ((x = y) -> (eq x y))).
Proof.
intros x y h1 h2 h3.
rewrite h3.
apply (eq_not_nan_refl (is_finite_not_nan h2)).
Qed.

(* Why3 goal *)
Lemma eq_refl : forall (x:t), (is_finite x) -> (eq x x).
Proof.
intros x h1.
apply (eq_not_nan_refl (is_finite_not_nan h1)).
Qed.

(* Why3 goal *)
Lemma eq_sym : forall (x:t) (y:t), (eq x y) -> (eq y x).
Proof.
intros x y.
unfold eq; intro h; rewrite Bcompare_swap, h; easy.
Qed.

(* Why3 goal *)
Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x
  z)).
Proof.
  intros x y z h1 h2.
  destruct x, y, z; auto; destruct b, b0, b1; auto; try easy;
  apply to_real_eq in h1; try (split;easy);
  apply to_real_eq in h2; try (split;easy);
  apply to_real_eq; try (split;easy);
  apply (eq_trans h1 h2).
Qed.

(* Why3 goal *)
Lemma eq_zero : (eq zeroF (neg zeroF)).
Proof.
easy.
Qed.

(* Why3 goal *)
Lemma eq_to_real_finite : forall (x:t) (y:t), ((is_finite x) /\ (is_finite
  y)) -> ((eq x y) <-> ((to_real x) = (to_real y))).
Proof.
intros x y (h1,h2).
apply (to_real_eq h1 h2).
Qed.

(* Why3 goal *)
Lemma eq_special : forall (x:t) (y:t), (eq x y) -> ((is_not_nan x) /\
  ((is_not_nan y) /\ (((is_finite x) /\ (is_finite y)) \/ ((is_infinite x) /\
  ((is_infinite y) /\ (same_sign x y)))))).
Proof.
  intros x y h1.
  rewrite is_not_nan1, is_not_nan1.
  destruct (eq_not_nan h1) as (h2,h3).
  split; [auto|split;auto].
  destruct (not_nan _ h2); [left|right].
  - split; [apply i|apply (eq_finite_dist h1 i)].
  - split; [apply i|split;[apply (eq_infinite_dist h1 i)|]].
    destruct x, y; destruct b, b0; auto; easy.
Qed.

(* Why3 goal *)
Lemma lt_finite : forall (x:t) (y:t), ((is_finite x) /\ (is_finite y)) ->
  ((lt x y) <-> ((to_real x) < (to_real y))%R).
Proof.
intros x y (h1,h2).
unfold lt.
rewrite (Bcompare_correct _ _ x y h1 h2), Some_ext.
split; intro H; [apply (Rcompare_Lt_inv _ _ H)|
                 apply (Rcompare_Lt _ _ H)].
Qed.

(* Why3 goal *)
Lemma le_finite : forall (x:t) (y:t), ((is_finite x) /\ (is_finite y)) ->
  ((le x y) <-> ((to_real x) <= (to_real y))%R).
Proof.
intros x y (h1,h2).
unfold le.
rewrite (Bcompare_correct _ _ x y h1 h2), Some_ext, Some_ext.
split; intro H.
destruct H; [apply Rlt_le; apply (Rcompare_Lt_inv _ _ H)|
             apply Req_le; apply (Rcompare_Eq_inv _ _ H)].
destruct H; [left; apply (Rcompare_Lt _ _ H)|
             right; apply (Rcompare_Eq _ _ H)].
Qed.

Lemma lt_eq_trans : forall {x y z:t}, lt x y -> eq y z -> lt x z.
Proof.
  intros x y z h1 h2.
  destruct x, y, z; try easy; try (destruct b, b0, b1; easy).
  set (x:=B754_finite b m e e0);
    set (y:=B754_finite b0 m0 e1 e2);
    set (z:=B754_finite b1 m1 e3 e4); fold x y z in h1, h2.
  pose proof (Bcompare_correct sb emax x y).
  pose proof (Bcompare_correct sb emax y z).
  pose proof (Bcompare_correct sb emax x z).
  unfold lt in h1.
  rewrite H in h1 by easy; clear H.
  unfold eq in h2.
  rewrite H0 in h2 by easy; clear H0.
  unfold lt.
  rewrite H1 by easy; clear H1.
  apply f_equal, Rcompare_Lt.
  apply Rlt_le_trans with (B2R sb emax (B754_finite b0 m0 e1 e2)).
  + apply Rcompare_Lt_inv.
    now injection h1.
  + apply Rcompare_not_Gt_inv.
    inversion h1; inversion h2.
    destruct Rcompare; try easy.
    destruct Rcompare; try easy;
    simpl; rewrite H1; discriminate.
Qed.

Lemma eq_lt_trans : forall {x y z:t}, eq x y -> lt y z -> lt x z.
Proof.
  intros x y z h1 h2.
  destruct x, y, z; try easy; try (destruct b, b0, b1; easy).
  set (x:=B754_finite b m e e0);
    set (y:=B754_finite b0 m0 e1 e2);
    set (z:=B754_finite b1 m1 e3 e4); fold x y z in h1, h2.
  pose proof (Bcompare_correct sb emax x y).
  pose proof (Bcompare_correct sb emax y z).
  pose proof (Bcompare_correct sb emax x z).
  unfold eq in h1.
  unfold lt in h2.
  rewrite H in h1 by easy; clear H.
  rewrite H0 in h2 by easy; clear H0.
  unfold lt.
  rewrite H1 by easy; clear H1.
  apply f_equal, Rcompare_Lt.
  apply Rle_lt_trans with (B2R sb emax (B754_finite b0 m0 e1 e2)).
  + apply Rcompare_not_Gt_inv.
    inversion h1; inversion h2.
    destruct Rcompare; try easy;
    simpl; rewrite H0; discriminate.
  + apply Rcompare_Lt_inv.
    now injection h2.
Qed.

Lemma lt_lt_trans : forall {x y z:t}, lt x y -> lt y z -> lt x z.
Proof.
  intros x y z h1 h2.
  destruct x, y, z; try easy; try (destruct b, b0, b1; easy).
  set (x:=B754_finite b m e e0);
    set (y:=B754_finite b0 m0 e1 e2);
    set (z:=B754_finite b1 m1 e3 e4); fold x y z in h1, h2.
  pose proof (Bcompare_correct sb emax x y).
  pose proof (Bcompare_correct sb emax y z).
  pose proof (Bcompare_correct sb emax x z).
  unfold lt in h1, h2.
  rewrite H in h1 by easy; clear H.
  rewrite H0 in h2 by easy; clear H0.
  unfold lt.
  rewrite H1 by easy; clear H1.
  apply f_equal, Rcompare_Lt.
  apply Rlt_trans with (B2R sb emax (B754_finite b0 m0 e1 e2)).
  + apply Rcompare_Lt_inv.
    now injection h1.
  + apply Rcompare_Lt_inv.
    now injection h2.
Qed.

(* Why3 goal *)
Lemma le_lt_trans : forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x
  z).
Proof.
  intros x y z (h,h1).
  destruct h as [h|h].
  apply (lt_lt_trans h h1).
  apply (eq_lt_trans h h1).
Qed.

(* Why3 goal *)
Lemma lt_le_trans : forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x
  z).
Proof.
  intros x y z (h1,h2).
  destruct h2 as [h2|h2].
  apply (lt_lt_trans h1 h2).
  apply (lt_eq_trans h1 h2).
Qed.

(* Why3 goal *)
Lemma le_ge_asym : forall (x:t) (y:t), ((le x y) /\ (le y x)) -> (eq x y).
Proof.
intros x y.
unfold le, eq.
destruct x, y; intros (h,h1); auto; try (destruct b,b0,h,h1; easy).
set (x:=B754_finite b m e e0);
  set (y:=B754_finite b0 m0 e1 e2);
  fold x y in h, h1.
pose proof (Bcompare_correct sb emax x y).
pose proof (Bcompare_correct sb emax y x).
rewrite H in h by easy.
rewrite H0 in h1 by easy.
rewrite H by easy.
f_equal.
apply Rcompare_Eq.
apply Rle_antisym.
+ apply Rcompare_not_Gt_inv.
  destruct Rcompare.
  easy.
  easy.
  destruct h as [h|h]; inversion h.
+ apply Rcompare_not_Gt_inv.
  destruct (Rcompare (B2R sb emax y) (B2R sb emax x)).
  easy.
  easy.
  destruct h1 as [h1|h1]; inversion h1.
Qed.

Lemma Some_ext_op: forall {T} (a b:T), Some a <> Some b <-> a <> b.
Proof.
  intros; split; intro H.
  intro h.
  apply (H (f_equal _ h)).
  intro h; injection h; auto.
Qed.

(* Why3 goal *)
Lemma not_lt_ge : forall (x:t) (y:t), ((~ (lt x y)) /\ ((is_not_nan x) /\
  (is_not_nan y))) -> (le y x).
Proof.
  intros x y.
  rewrite is_not_nan1; rewrite is_not_nan1.
  unfold is_nan.
  destruct x, y; intros (h,(h1,h2)); auto; try (destruct b, b0; auto; destruct h1; auto; easy).
  set (x:=B754_finite b m e e0);
    set (y:=B754_finite b0 m0 e1 e2);
    fold x y in h, h1, h2.
  pose proof (Bcompare_correct sb emax x y).
  pose proof (Bcompare_correct sb emax y x).
  try easy;
  unfold le; unfold lt in h.
  rewrite H in h by easy.
  rewrite H0 by easy.
  rewrite Some_ext_op in h.
  destruct (Rcompare_not_Lt_inv _ _ h);
    [left;f_equal; apply Rcompare_Lt; assumption|
     right;f_equal; apply Rcompare_Eq; assumption].
Qed.

(* Why3 goal *)
Lemma not_gt_le : forall (x:t) (y:t), ((~ (lt y x)) /\ ((is_not_nan x) /\
  (is_not_nan y))) -> (le x y).
Proof.
  intros x y.
  rewrite is_not_nan1; rewrite is_not_nan1.
  unfold is_nan.
  destruct x, y; intros (h,(h1,h2)); auto; try (destruct b, b0; auto; destruct h1; auto; easy).
  set (x:=B754_finite b m e e0);
    set (y:=B754_finite b0 m0 e1 e2);
    fold x y in h, h1, h2.
  pose proof (Bcompare_correct sb emax x y).
  pose proof (Bcompare_correct sb emax y x).
  unfold le; unfold lt in h.
  rewrite H0 in h by easy.
  rewrite H by easy.
  rewrite Some_ext_op in h.
  destruct (Rcompare_not_Lt_inv _ _ h);
    [left;f_equal; apply Rcompare_Lt; assumption|
     right;f_equal; apply Rcompare_Eq; assumption].
Qed.

(* Why3 goal *)
Lemma le_special : forall (x:t) (y:t), (le x y) -> (((is_finite x) /\
  (is_finite y)) \/ (((is_minus_infinity x) /\ (is_not_nan y)) \/
  ((is_not_nan x) /\ (is_plus_infinity y)))).
Proof.
  intros x y h.
  rewrite is_not_nan1; rewrite is_not_nan1.
  unfold le in h.
  unfold is_nan, is_finite.
  destruct x, y; auto; try easy; try (destruct b, b0; auto; destruct h; auto; easy).
  - right; right. destruct b0, h; split; easy.
  - right; left. destruct b, h; split; easy.
  - right. destruct b, b0, h; try easy.
    + left; split; easy.
    + left; split; easy.
    + right; split; easy.
  - right; left. destruct b, h; split; easy.
  - right; right. destruct b, b0, h; split; easy.
Qed.

(* Why3 goal *)
Lemma lt_special : forall (x:t) (y:t), (lt x y) -> (((is_finite x) /\
  (is_finite y)) \/ (((is_minus_infinity x) /\ ((is_not_nan y) /\
  ~ (is_minus_infinity y))) \/ ((is_not_nan x) /\ ((~ (is_plus_infinity
  x)) /\ (is_plus_infinity y))))).
Proof.
  intros x y h.
  rewrite is_not_nan1; rewrite is_not_nan1.
  unfold lt in h.
  unfold is_nan, is_finite.
  unfold is_plus_infinity, is_minus_infinity.
  destruct x, y; auto; try easy; try (destruct b, b0; easy).

  - right; right. destruct b0; split; try split; easy.
  - right; left. destruct b; split; try split; easy.
  - right; right. destruct b, b0; split; try split; easy.
  - right; left. destruct b; split; try split; easy.
  - right; right. destruct b, b0; split; try split; easy.
Qed.

(* Why3 goal *)
Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) ->
  (is_finite y)).
Proof.
intros x y z h1 h2.
destruct x, y, z; destruct b, b0, b1; easy.
Qed.

(* Why3 goal *)
Lemma positive_to_real : forall (x:t), (is_finite x) -> ((is_positive x) ->
  (0%R <= (to_real x))%R).
Proof.
  intros x h1 h2.
  assert (is_finite zeroF) as zero_is_finite by easy.
  rewrite <-zeroF_to_real; apply (le_to_real _ _ zero_is_finite h1).
  generalize (is_positive_correct x); intro H; destruct H, H; auto.
  rewrite H; auto.
Qed.

Lemma non_zero_positive_to_real : forall {x:t},
    is_finite x -> ~ is_zero x -> is_positive x ->
     0 < to_real x.
Proof.
  intros x h1 h2 h3.
  rewrite <-zeroF_to_real; apply lt_finite.
  split; easy.
  destruct x; try easy.
  contradict h2; easy.
  simpl in h3.
  destruct b; simpl; easy.
Qed.

Lemma is_positive_to_int: forall {x} {m:mode}, is_finite x -> is_positive x -> (0 <= to_int m x)%Z.
Proof.
  intros x m h h1.
  rewrite <-(to_int_zeroF m).
  destruct (valid_rnd_round_mode m) as (h2,_).
  destruct m; simpl in h2; apply h2; now apply positive_to_real.
Qed.

(* Why3 goal *)
Lemma to_real_positive : forall (x:t), (is_finite x) ->
  ((0%R < (to_real x))%R -> (is_positive x)).
Proof.
  intros x h1 h2.
  assert (is_finite zeroF) as zero_is_finite by easy.
  rewrite <-zeroF_to_real, <-(lt_finite _ _ (conj zero_is_finite h1)) in h2.
  generalize (is_positive_correct x); intro H; destruct H; auto.
Qed.

(* Why3 goal *)
Lemma negative_to_real : forall (x:t), (is_finite x) -> ((is_negative x) ->
  ((to_real x) <= 0%R)%R).
Proof.
  intros x h1 h2.
  assert (is_finite zeroF) as zero_is_finite by easy.
  rewrite <-zeroF_to_real; apply (le_to_real _ _ h1 zero_is_finite).
  generalize (is_negative_correct x); intro H; destruct H, H; auto.
  rewrite H; auto.
Qed.

Lemma non_zero_negative_to_real : forall {x:t},
    is_finite x -> ~ is_zero x -> is_negative x ->
     to_real x < 0.
Proof.
  intros x h1 h2 h3.
  rewrite <-zeroF_to_real; apply lt_finite.
  split; easy.
  destruct x; try easy.
  contradict h2; easy.
  simpl in h3.
  destruct b; simpl; easy.
Qed.

Lemma is_negative_to_int: forall {x} {m:mode}, is_finite x -> is_negative x -> (to_int m x <= 0)%Z.
Proof.
  intros x m h h1.
  rewrite <-(to_int_zeroF m).
  destruct (valid_rnd_round_mode m) as (h2,_).
  destruct m; simpl in h2; apply h2; now apply negative_to_real.
Qed.

(* Why3 goal *)
Lemma to_real_negative : forall (x:t), (is_finite x) ->
  (((to_real x) < 0%R)%R -> (is_negative x)).
Proof.
  intros x h1 h2.
  assert (is_finite zeroF) as zero_is_finite by easy.
  rewrite <-zeroF_to_real, <-(lt_finite _ _ (conj h1 zero_is_finite)) in h2.
  generalize (is_negative_correct x); intro H; destruct H; auto.
Qed.

(* Why3 goal *)
Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\
  (is_negative x)).
Proof.
intros x.
destruct x ; destruct b; easy.
Qed.

(* Why3 goal *)
Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive
  x) \/ (is_negative x)).
Proof.
intros x h1.
destruct x ; destruct b; simpl; auto; now elim h1.
Qed.

(* Why3 goal *)
Lemma diff_sign_trans : forall (x:t) (y:t) (z:t), ((diff_sign x y) /\
  (diff_sign y z)) -> (same_sign x z).
Proof.
  unfold diff_sign, same_sign.
  intros x y z (h1,h2).
  pose proof (negative_xor_positive y) as H.
  destruct h1 as [(h,h1)|(h,h1)], h2 as [(h2,h3)|(h2,h3)].
  - contradict H; split; easy.
  - left; split; easy.
  - right; split; easy.
  - contradict H; split; easy.
Qed.

(* Why3 goal *)
Lemma diff_sign_product : forall (x:t) (y:t), ((is_finite x) /\ ((is_finite
  y) /\ (((to_real x) * (to_real y))%R < 0%R)%R)) -> (diff_sign x y).
Proof.
intros x y (h1,(h2,h3)).
unfold diff_sign.
case (Rcase_abs (to_real y)); intro; [left|right].
- split; [apply to_real_positive; try easy|apply to_real_negative; easy].
  apply Rmult_lt_reg_r with (r := (-to_real y)); try fourier.
  rewrite Rmult_0_l, Ropp_mult_distr_r_reverse.
  apply Ropp_0_gt_lt_contravar.
  fourier.
- destruct r.
  + split; [apply to_real_negative; try easy|apply to_real_positive; easy].
    apply Rmult_lt_reg_r with (r := (to_real y)); try fourier.
  + assert false;[|easy].
    rewrite H in h3; fourier.
Qed.

(* Why3 goal *)
Lemma same_sign_product : forall (x:t) (y:t), ((is_finite x) /\ ((is_finite
  y) /\ (same_sign x y))) -> (0%R <= ((to_real x) * (to_real y))%R)%R.
Proof.
intros x y (h1,(h2,h3)).
unfold same_sign in h3.
destruct h3 as [(h3,h4)|(h3,h4)].
- apply (positive_to_real _ h1) in h3.
  apply (positive_to_real _ h2) in h4.
  apply Rmult_le_pos; auto.
- apply (negative_to_real _ h1) in h3.
  apply (negative_to_real _ h2) in h4.
  rewrite <-Rmult_opp_opp.
  apply Rmult_le_pos; fourier.
Qed.

(* Why3 assumption *)
Definition product_sign (z:t) (x:t) (y:t): Prop := ((same_sign x y) ->
  (is_positive z)) /\ ((diff_sign x y) -> (is_negative z)).

(* Why3 assumption *)
Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t): Prop :=
  match m with
  | ieee_float.RoundingMode.RTN => ((is_positive x) -> ((is_finite x) /\
      ((to_real x) = max_real))) /\ ((~ (is_positive x)) -> (is_infinite x))
  | ieee_float.RoundingMode.RTP => ((is_positive x) -> (is_infinite x)) /\
      ((~ (is_positive x)) -> ((is_finite x) /\
      ((to_real x) = (-max_real)%R)))
  | ieee_float.RoundingMode.RTZ => ((is_positive x) -> ((is_finite x) /\
      ((to_real x) = max_real))) /\ ((~ (is_positive x)) -> ((is_finite x) /\
      ((to_real x) = (-max_real)%R)))
  | (ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE) => (is_infinite
      x)
  end.

(* Why3 assumption *)
Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t): Prop :=
  (is_zero x) ->
  match m with
  | ieee_float.RoundingMode.RTN => (is_negative x)
  | _ => (is_positive x)
  end.

(* Why3 goal *)
Lemma add_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite x) -> ((is_finite y) -> ((no_overflow m
  ((to_real x) + (to_real y))%R) -> ((is_finite (add m x y)) /\
  ((to_real (add m x y)) = (round m ((to_real x) + (to_real y))%R))))).
Proof.
intros m x y h1 h2 h3.
generalize (Bplus_correct sb emax Hsb'' Hemax' nan_bf m x y h1 h2); rewrite Rlt_bool_true.
intro; split; easy.
apply (in_range_bpow_radix2_emax _ h3).
Qed.

(* Why3 goal *)
Lemma add_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite (add m x y)) -> ((is_finite x) /\ (is_finite y)).
Proof.
intros m x y h1.
destruct x, y; try easy; destruct b, b0; easy.
Qed.

(* Why3 goal *)
Lemma add_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> ((is_finite (add m x y)) ->
  ((no_overflow m ((to_real x) + (to_real y))%R) /\ ((to_real (add m x
  y)) = (round m ((to_real x) + (to_real y))%R)))).
Proof.
intros m x y h1 h2.
destruct (add_finite_rev m x y h2).
assert (no_overflow m (to_real x + to_real y)).
2: split; [easy|apply add_finite; easy].
pose proof max_real_ge_6.
destruct x, y; try easy; try (rewrite B754_zero_to_real).
apply Bounded_real_no_overflow; rewrite (@B754_zero_to_real b0); split; fourier.
apply Bounded_real_no_overflow; rewrite Rplus_0_l; apply is_finite1; auto.
apply Bounded_real_no_overflow; rewrite Rplus_0_r; apply is_finite1; auto.
set (x := B754_finite b m0 e e0).
set (y := B754_finite b0 m1 e1 e2).
fold x y in h2, H, H0.
destruct (Rlt_le_dec (Rabs (round m (to_real x + to_real y))) (bpow radix2 emax)).
rewrite no_overflow_Rabs_round_emax; assumption.
pose proof (Bplus_correct sb emax Hsb'' Hemax' nan_bf m x y H H0).
change (Bplus sb emax Hsb'' Hemax' nan_bf m) with (add m) in H2.
rewrite Rlt_bool_false in H2; auto.
destruct m, h1; try easy.
destruct (add RNE x y); easy.
destruct (add RNA x y); easy.
Qed.

(* Why3 goal *)
Lemma sub_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite x) -> ((is_finite y) -> ((no_overflow m
  ((to_real x) - (to_real y))%R) -> ((is_finite (sub m x y)) /\
  ((to_real (sub m x y)) = (round m ((to_real x) - (to_real y))%R))))).
Proof.
intros m x y h1 h2 h3.
generalize (Bminus_correct sb emax Hsb'' Hemax' nan_bf m x y h1 h2); rewrite Rlt_bool_true.
intro; split; easy.
apply (in_range_bpow_radix2_emax _ h3).
Qed.

(* Why3 goal *)
Lemma sub_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite (sub m x y)) -> ((is_finite x) /\ (is_finite y)).
Proof.
  intros m x y h1.
  destruct x, y; try easy; destruct b, b0; easy.
Qed.

(* Why3 goal *)
Lemma sub_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> ((is_finite (sub m x y)) ->
  ((no_overflow m ((to_real x) - (to_real y))%R) /\ ((to_real (sub m x
  y)) = (round m ((to_real x) - (to_real y))%R)))).
Proof.
intros m x y h1 h2.
destruct (sub_finite_rev m x y h2).
assert (no_overflow m (to_real x - to_real y)).
2: split; [easy|apply sub_finite; easy].
pose proof max_real_ge_6.
destruct x, y; try easy; try (rewrite B754_zero_to_real).
apply Bounded_real_no_overflow; rewrite (@B754_zero_to_real b0); split; fourier.
apply Bounded_real_no_overflow.
unfold to_real.
rewrite Rminus_0_l, <-(B2R_Bopp _ _ pair).
apply is_finite1, is_finite_Bopp.
apply Bounded_real_no_overflow; rewrite Rminus_0_r; apply is_finite1; auto.
set (x := B754_finite b m0 e e0).
set (y := B754_finite b0 m1 e1 e2).
fold x y in h2, H, H0.
destruct (Rlt_le_dec (Rabs (round m (to_real x - to_real y))) (bpow radix2 emax)).
rewrite no_overflow_Rabs_round_emax; assumption.
pose proof (Bminus_correct sb emax Hsb'' Hemax' nan_bf m x y H H0).
change (Bminus sb emax Hsb'' Hemax' nan_bf m) with (sub m) in H2.
rewrite Rlt_bool_false in H2; auto.
destruct m, h1; try easy.
destruct (sub RNE x y); easy.
destruct (sub RNA x y); easy.
Qed.

(* Why3 goal *)
Lemma mul_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite x) -> ((is_finite y) -> ((no_overflow m
  ((to_real x) * (to_real y))%R) -> ((is_finite (mul m x y)) /\
  ((to_real (mul m x y)) = (round m ((to_real x) * (to_real y))%R))))).
Proof.
intros m x y h1 h2 h3.
generalize (Bmult_correct sb emax Hsb'' Hemax' nan_bf m x y); rewrite Rlt_bool_true, h1, h2.
intro; split; easy.
apply (in_range_bpow_radix2_emax _ h3).
Qed.

(* Why3 goal *)
Lemma mul_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite (mul m x y)) -> ((is_finite x) /\ (is_finite y)).
Proof.
  intros m x y h1.
  destruct x, y; try easy; destruct b, b0; easy.
Qed.

(* Why3 goal *)
Lemma mul_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> ((is_finite (mul m x y)) ->
  ((no_overflow m ((to_real x) * (to_real y))%R) /\ ((to_real (mul m x
  y)) = (round m ((to_real x) * (to_real y))%R)))).
Proof.
intros m x y h1 h2.
destruct (mul_finite_rev m x y h2).
assert (no_overflow m (to_real x * to_real y)).
2: split; [easy|apply mul_finite; easy].
pose proof max_real_ge_6.
destruct x, y; try easy; try (rewrite B754_zero_to_real).
apply Bounded_real_no_overflow; rewrite (@B754_zero_to_real b0); split; fourier.
unfold no_overflow; rewrite Rmult_0_l, <-zeroF_to_real, Round_to_real, zeroF_to_real; auto; split; fourier.
unfold no_overflow; rewrite Rmult_0_r, <-zeroF_to_real, Round_to_real, zeroF_to_real; auto; split; fourier.
set (x := B754_finite b m0 e e0).
set (y := B754_finite b0 m1 e1 e2).
fold x y in h2, H, H0.
destruct (Rlt_le_dec (Rabs (round m (to_real x * to_real y))) (bpow radix2 emax)).
rewrite no_overflow_Rabs_round_emax; assumption.
pose proof (Bmult_correct sb emax Hsb'' Hemax' nan_bf m x y).
change (Bmult sb emax Hsb'' Hemax' nan_bf m) with (mul m) in H2.
rewrite Rlt_bool_false in H2; auto.
destruct m, h1; try easy.
destruct (mul RNE x y); easy.
destruct (mul RNA x y); easy.
Qed.

(* Why3 goal *)
Lemma div_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite x) -> ((is_finite y) -> ((~ (is_zero y)) -> ((no_overflow m
  ((to_real x) / (to_real y))%R) -> ((is_finite (div m x y)) /\
  ((to_real (div m x y)) = (round m ((to_real x) / (to_real y))%R)))))).
Proof.
  intros m x y h1 h2 h3 h4.
  assert (is_finite zeroF) as zero_is_finite by easy.
  rewrite (to_real_eq zero_is_finite h2) in h3.
  apply not_eq_sym in h3.
  generalize (Bdiv_correct sb emax Hsb'' Hemax' nan_bf m x y h3); rewrite Rlt_bool_true, h1.
  intro; split; easy.
  apply (in_range_bpow_radix2_emax _ h4).
Qed.

(* Why3 goal *)
Lemma div_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite (div m x y)) -> (((is_finite x) /\ ((is_finite y) /\ ~ (is_zero
  y))) \/ ((is_finite x) /\ ((is_infinite y) /\ ((to_real (div m x
  y)) = 0%R)))).
Proof.
  intros m x y h1.
  destruct x, y; try easy.
  right; destruct b, b0; easy.
  left; destruct b, b0; split; try split; easy.
  right; destruct b, b0; split; try split; easy.
  left; destruct b, b0; split; try split; easy.
Qed.

(* Why3 goal *)
Lemma div_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> ((is_finite (div m x y)) ->
  ((is_finite y) -> ((no_overflow m ((to_real x) / (to_real y))%R) /\
  ((to_real (div m x y)) = (round m ((to_real x) / (to_real y))%R))))).
Proof.
  intros m x y h1 h2 h3.
  destruct (div_finite_rev m x y h2) as [(h4,(h5,h6))|(h4,(h5,h6))].
  + assert (no_overflow m (to_real x / to_real y)).
    2: split; [easy|apply div_finite; easy].
    pose proof max_real_ge_6.
    destruct x, y; try easy; try (rewrite B754_zero_to_real).
    rewrite Real.infix_sl_def, Rmult_0_l.
    apply Bounded_real_no_overflow; split; fourier.
    set (x := B754_finite b m0 e e0).
    set (y := B754_finite b0 m1 e1 e2).
    fold x y in h2, h3,h4,h5,h6.
    destruct (Rlt_le_dec (Rabs (round m (to_real x / to_real y))) (bpow radix2 emax)).
    rewrite no_overflow_Rabs_round_emax; assumption.
    assert (to_real y <> 0) by (rewrite zero_to_real in h6; auto).
    pose proof (Bdiv_correct sb emax Hsb'' Hemax' nan_bf m x y H0).
    change (Bdiv sb emax Hsb'' Hemax' nan_bf m) with (div m) in H1.
    rewrite Rlt_bool_false in H1; auto.
    destruct m, h1; try easy.
    destruct (div RNE x y); easy.
    destruct (div RNA x y); easy.
  + destruct y; easy.
Qed.

(* Why3 goal *)
Lemma neg_finite : forall (x:t), (is_finite x) -> ((is_finite (neg x)) /\
  ((to_real (neg x)) = (-(to_real x))%R)).
Proof.
intros x h1.
split.
unfold neg, is_finite.
rewrite is_finite_Bopp; apply h1.
apply B2R_Bopp.
Qed.

(* Why3 goal *)
Lemma neg_finite_rev : forall (x:t), (is_finite (neg x)) -> ((is_finite x) /\
  ((to_real (neg x)) = (-(to_real x))%R)).
Proof.
  intros x h1.
  assert (is_finite x) by (destruct x; easy).
  split; [easy| apply neg_finite; auto].
Qed.

(* Why3 goal *)
Lemma abs_finite : forall (x:t), (is_finite x) -> ((is_finite (abs x)) /\
  (((to_real (abs x)) = (Reals.Rbasic_fun.Rabs (to_real x))) /\ (is_positive
  (abs x)))).
Proof.
  intros x h1.
  pose proof (is_finite_abs x h1).
  split;[assumption|split].
  apply B2R_Babs.
  pose proof (is_finite_not_nan h1).
  pose proof (Bsign_Babs sb emax pair x).
  apply is_positive_Bsign.
  apply (is_finite_not_nan H).
  apply H1.
  now apply Bool.not_true_is_false.
Qed.

(* add to theory ? *)
Lemma abs_le: forall {x y}, le (neg y) x /\ le x y -> le (abs x) y.
Proof.
  intros x y.
  destruct (Finite_Infinite_Nan_dec y) as [[hy|hy]|hy].
  + destruct (Finite_Infinite_Nan_dec x) as [[hx|hx]|hx].

    * pose proof (is_finite_abs _ hx).
      destruct (neg_finite _ hy).
      rewrite (le_to_real (abs x) y) by auto.
      rewrite (le_to_real (neg y) x) by auto.
      rewrite le_to_real by auto.
      rewrite H1 by auto.
      destruct (abs_finite _ hx) as (_,(u,_)).
      rewrite u.
      apply Rabs_le.

    * intros (a,b).
      destruct (le_special _ _ b) as [H|[H|H]].
      - destruct x; easy.
      - pose proof (le_special _ _ a).
        unfold is_minus_infinity, is_plus_infinity in H0.
        destruct H0, H0, x, y; auto; try easy; destruct b0, b1; auto.
      - destruct y; unfold is_plus_infinity in H; easy.

    * intros (a,b).
      destruct (le_special _ _ b) as [H|[H|H]];
        unfold is_minus_infinity in H;
        destruct x; easy.

  + intros (a,b).

    destruct (Finite_Infinite_Nan_dec x) as [[hx|hx]|hx].
    * destruct (le_special _ _ b) as [H|[H|H]].
      - destruct y; easy.
      - unfold is_minus_infinity in H; destruct x; easy.
      - destruct y, H as (H,(_,H')); destruct b0; try easy.
        assert (~ is_nan x) by (rewrite <-is_not_nan1; assumption).
        apply le_infinity.
        destruct x; easy.
    * destruct x, y; try easy.
      unfold le, Bcompare.
      destruct b1; [|right; reflexivity].
      destruct b0; easy.
    * destruct x; unfold le, Bcompare in b; easy.

  + intros (_,a).
    destruct y; unfold le, Bcompare in a; try easy.
    destruct x as [b0|b0|b0|b0]; destruct b0; easy.
Qed.

(* Why3 goal *)
Lemma abs_finite_rev : forall (x:t), (is_finite (abs x)) -> ((is_finite x) /\
  ((to_real (abs x)) = (Reals.Rbasic_fun.Rabs (to_real x)))).
Proof.
intros x h1.
assert (is_finite x) by (destruct x; easy).
split; [easy| apply abs_finite; auto].
Qed.

(* Why3 goal *)
Lemma abs_universal : forall (x:t), ~ (is_negative (abs x)).
Proof.
destruct x; easy.
Qed.

(* Why3 goal *)
Lemma fma_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t) (z:t),
  (is_finite x) -> ((is_finite y) -> ((is_finite z) -> ((no_overflow m
  (((to_real x) * (to_real y))%R + (to_real z))%R) -> ((is_finite (fma m x y
  z)) /\ ((to_real (fma m x y z)) = (round m
  (((to_real x) * (to_real y))%R + (to_real z))%R)))))).
Proof.
intros m x y z h1 h2 h3 h4.
Admitted.

(* Why3 goal *)
Lemma fma_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t)
  (z:t), (is_finite (fma m x y z)) -> ((is_finite x) /\ ((is_finite y) /\
  (is_finite z))).
Proof.
intros m x y z h1.
Admitted.

(* Why3 goal *)
Lemma fma_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t)
  (z:t), (ieee_float.RoundingMode.to_nearest m) -> ((is_finite (fma m x y
  z)) -> ((no_overflow m (((to_real x) * (to_real y))%R + (to_real z))%R) /\
  ((to_real (fma m x y z)) = (round m
  (((to_real x) * (to_real y))%R + (to_real z))%R)))).
Proof.
intros m x y z h1 h2.
Admitted.

(* Why3 goal *)
Lemma sqrt_finite : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_finite
  x) -> ((0%R <= (to_real x))%R -> ((is_finite (sqrt m x)) /\
  ((to_real (sqrt m x)) = (round m (Reals.R_sqrt.sqrt (to_real x)))))).
Proof.
  intros m x h1 h2.
  destruct (Bsqrt_correct sb emax Hsb' Hemax' (fun b => (true,One_Nan_pl)) m x) as (g,(g1,g2)).
  split; auto.
  destruct x ; destruct b; try easy.
  contradict h2.
  apply Rlt_not_le, non_zero_negative_to_real; easy.
Qed.

(* Why3 goal *)
Lemma sqrt_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (is_finite (sqrt m x)) -> ((is_finite x) /\ ((0%R <= (to_real x))%R /\
  ((to_real (sqrt m x)) = (round m (Reals.R_sqrt.sqrt (to_real x)))))).
Proof.
  intros m x h1.
  assert (is_finite x) by (destruct x ; destruct b; easy).
  split; [easy|].
  assert (0 <= to_real x).
  { destruct x ; destruct b; try easy.
    rewrite (@B754_zero_to_real true); fourier.
    rewrite (@B754_zero_to_real false); fourier.
    assert (is_positive (B754_finite false m0 e e0)) by easy.
    apply positive_to_real; auto. }
  split; [easy| apply sqrt_finite; auto].
Qed.

(* Why3 assumption *)
Definition same_sign_real (x:t) (r:R): Prop := ((is_positive x) /\
  (0%R < r)%R) \/ ((is_negative x) /\ (r < 0%R)%R).

Lemma sign_FF_overflow : forall m b,
    sign_FF (binary_overflow sb emax m b) = b.
Proof.
  intros m b.
  unfold binary_overflow.
  destruct (overflow_to_inf m b); auto.
Qed.

Lemma sign_FF_B2FF : forall x, sign_FF (B2FF sb emax x) = Bsign sb emax x.
Proof.
  destruct x; try easy.
  destruct n; easy.
Qed.

(* Why3 goal *)
Lemma add_special : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  let r := (add m x y) in ((((is_nan x) \/ (is_nan y)) -> (is_nan r)) /\
  ((((is_finite x) /\ (is_infinite y)) -> ((is_infinite r) /\ (same_sign r
  y))) /\ ((((is_infinite x) /\ (is_finite y)) -> ((is_infinite r) /\
  (same_sign r x))) /\ ((((is_infinite x) /\ ((is_infinite y) /\ (same_sign x
  y))) -> ((is_infinite r) /\ (same_sign r x))) /\ ((((is_infinite x) /\
  ((is_infinite y) /\ (diff_sign x y))) -> (is_nan r)) /\ ((((is_finite x) /\
  ((is_finite y) /\ ~ (no_overflow m ((to_real x) + (to_real y))%R))) ->
  ((same_sign_real r ((to_real x) + (to_real y))%R) /\ (overflow_value m
  r))) /\ (((is_finite x) /\ (is_finite y)) -> (((same_sign x y) ->
  (same_sign r x)) /\ ((~ (same_sign x y)) -> (sign_zero_result m
  r)))))))))).
Proof.
intros m x y r.
  unfold same_sign, diff_sign, same_sign, same_sign_real.
  split;[intro h|split;[intros (h,h1)|split;[intros (h,h1)|split;[intros (h,(h1,h2))|split;[intros (h,(h1,h2))|split;[intros (h,(h1,h2))|split;[intro h|intro h]]]]]]].
  - destruct x, y; destruct b, b0, h; easy.
  - destruct x, y; destruct b0; auto; easy.
  - destruct x, y; destruct b; auto; easy.
  - destruct x, y; destruct b, b0; destruct h2 as [(h2,h3)|(h2,h3)]; auto; easy.
  - destruct x, y; destruct b, b0; destruct h2 as [(h2,h3)|(h2,h3)]; auto; easy.
  - rewrite no_overflow_Rabs_round_max_real, Rabs_round_max_real_emax in h2.
    apply Rnot_lt_le in h2.
    pose proof (Bplus_correct sb emax Hsb' Hemax' nan_bf m x y h h1).
    rewrite Rlt_bool_false in H by auto.
    destruct H.
    split.

    + destruct x, y; try easy.
      * destruct b, b0, m; simpl in H; easy.
      * rewrite B754_zero_to_real at 1 2.
        rewrite Rplus_0_l.
        rewrite <-(@B754_zero_to_real false) at 1 2.
        destruct b0;[right;split;[easy|]|left;split;[easy|]]; apply lt_finite; easy.
      * rewrite B754_zero_to_real at 1 2.
        rewrite Rplus_0_r.
        rewrite <-(@B754_zero_to_real false) at 1 2.
        destruct b;[right;split;[easy|]|left;split;[easy|]]; apply lt_finite; easy.
      * change (Bplus sb emax Hsb' Hemax' nan_bf m (B754_finite b m0 e e0) (B754_finite b0 m1 e1 e2)) with r in H.
        pose proof (sign_FF_overflow m (Bsign sb emax (B754_finite b m0 e e0))).
        rewrite <-H in H1.
        rewrite sign_FF_B2FF in H1.
        simpl Bsign at 2 in H1.
        assert (~is_nan r).
        { simpl binary_overflow in H.
          unfold binary_overflow in H.
          destruct overflow_to_inf in H;
            destruct r; try easy;
              destruct n; easy. }

        simpl in H0. {
        destruct b;rewrite <-H0;[right|left]; split.

        - rewrite <-is_negative_Bsign in H1; auto.
        - assert (to_real (B754_finite true m0 e e0) < 0) by
              (apply non_zero_negative_to_real; easy).
          assert (to_real (B754_finite true m1 e1 e2) < 0) by
              (apply non_zero_negative_to_real; easy).
          fourier.
        - rewrite <-is_positive_Bsign in H1; auto.
        - assert (0 < to_real (B754_finite false m0 e e0)) by
              (apply non_zero_positive_to_real; easy).
          assert (0 < to_real (B754_finite false m1 e1 e2)) by
              (apply non_zero_positive_to_real; easy).
          fourier. }

    + change (Bplus sb emax Hsb' Hemax' nan_bf m x y) with r in H.
      assert (H':=H).
      apply (f_equal sign_FF) in H'.
      rewrite sign_FF_B2FF, sign_FF_overflow in H'.
      destruct m; simpl;
        unfold binary_overflow in H;
        simpl in H.
      * destruct r; try easy; destruct n; easy.
      * destruct r; try easy; destruct n; easy.
      * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
            (destruct x ; destruct b; simpl; auto). {
        destruct H1; rewrite H1 in H', H0, H; simpl in H.
        - split.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H'; easy.
          intro; split.
          destruct r; try easy; destruct n; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H.
          + unfold to_real. rewrite <-min_real_is_F2R, <-FF2R_B2FF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
          apply Pos.pow_gt_1.
          zify; auto with zarith.
        - split.
          destruct r; easy.
          intro.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign in H2; auto; easy. }
      * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
            (destruct x ; destruct b; simpl; auto). {
        destruct H1; rewrite H1 in H', H0, H; simpl in H.
        - split.
          intro.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign in H2; auto. rewrite H' in H2; easy.
          destruct r; try easy; destruct n; easy.
        - split.
          intro; split.
          destruct r; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H.
          + unfold to_real. rewrite <-max_real_is_F2R, <-FF2R_B2FF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            apply Pos.pow_gt_1.
            zify; auto with zarith.
          + assert (~is_nan r) by
                (destruct r; try easy; destruct n; easy).
            rewrite is_positive_Bsign; easy. }
      * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
            (destruct x ; destruct b; simpl; auto).
        assert (~is_nan r) by
            (destruct H1, r; try easy; destruct n; easy).
        rewrite is_positive_Bsign; auto. {
        destruct H1; rewrite H1 in H', H0, H; simpl in H.
        - split.
          rewrite H'; easy.
          intro; split.
          destruct r; try easy; destruct n; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H.
          + unfold to_real. rewrite <-min_real_is_F2R, <-FF2R_B2FF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            apply Pos.pow_gt_1.
            zify; auto with zarith.
        - split.
          + intro; split.
            destruct r; try easy; destruct n; easy.
            replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H.
            * unfold to_real. rewrite <-max_real_is_F2R, <-FF2R_B2FF, H; auto.
            *  rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
               apply Pos.pow_gt_1.
               zify; auto with zarith.
           + easy. }
  - destruct H.
    pose proof (Bplus_correct sb emax Hsb' Hemax' nan_bf m x y H H0).
    destruct (Rlt_le_dec (Rabs (round m (to_real x + to_real y))) (bpow radix2 emax)).
    + rewrite Rlt_bool_true in H1; auto.
      destruct H1 as (h1,(h2,h3)).
      change (Bplus sb emax Hsb' Hemax' nan_bf m x y) with r in h1, h2, h3.
      assert (~is_nan r) by (destruct r; easy).
      destruct h as [(h,h')|(h,h')];[left|right];split;auto.
      * rewrite is_positive_Bsign; auto.
        destruct y; destruct b, x; destruct b; try easy.
        rewrite Rcompare_Gt in h3; auto.
        assert (0 < B2R sb emax (B754_finite false m0 e e0)) by
            (apply non_zero_positive_to_real; easy).
        assert (0 < B2R sb emax (B754_finite false m1 e1 e2)) by
            (apply non_zero_positive_to_real; easy).
        fourier.
      * rewrite is_negative_Bsign; auto.
        destruct y; destruct b,x; destruct b; try easy.
        rewrite Rcompare_Lt in h3; auto.
        assert (B2R sb emax (B754_finite true  m0 e e0) < 0) by
            (apply non_zero_negative_to_real; easy).
        assert (B2R sb emax (B754_finite true m1 e1 e2) < 0) by
            (apply non_zero_negative_to_real; easy).
        fourier.
    + rewrite Rlt_bool_false in H1; auto.
      destruct H1 as (h1,h2).
      change (Bplus sb emax Hsb' Hemax' nan_bf m x y) with r in h1.
      destruct (is_nan_dec r).
      destruct x; destruct b,y; destruct b; try easy; destruct m;
        unfold binary_overflow in h1; simpl in h1;
          destruct r; try easy; destruct n; easy.

      rewrite is_positive_Bsign; auto.
      rewrite is_negative_Bsign; auto.
      apply (f_equal sign_FF) in h1.
      rewrite sign_FF_B2FF, sign_FF_overflow in h1.
      assert (~is_nan x) by (destruct x; easy).
      rewrite is_positive_Bsign in h; auto.
      rewrite is_negative_Bsign in h; auto.
      destruct h as [(h,h')|(h,h')];rewrite h in h1, h2;[left|right];split;auto.
      rewrite is_positive_Bsign; auto.
      rewrite is_negative_Bsign; auto.
  - intuition.
    unfold sign_zero_result; intro.
    unfold is_zero in H2.
    rewrite eq_zero_iff in H2.
    pose proof (Bplus_correct sb emax Hsb' Hemax' nan_bf m x y H0 H1).
    destruct (Rlt_dec (Rabs (round m (to_real x + to_real y))) (bpow radix2 emax)) as [r0|r0];
      [rewrite Rlt_bool_true in H4; auto; clear r0|
       rewrite Rlt_bool_false in H4].
    + destruct H4 as (h1,(h2,h)).

      assert (to_real x + to_real y = 0).
      { apply (round_plus_eq_zero radix2 fexp (round_mode m)).
        apply generic_format_B2R.
        apply generic_format_B2R.
        destruct H2 as [H2|H2]; apply (f_equal to_real) in H2.
        rewrite zeroF_to_real in H2.
        rewrite <-H2; auto.
        assert (is_finite zeroF) as zero_is_finite by easy.
        destruct (neg_finite zeroF zero_is_finite).
        rewrite H5, zeroF_to_real, Ropp_0 in H2.
        rewrite <-H2; auto. }

      rewrite Rcompare_Eq in h; auto.
      replace (add m x y) with r in h by auto.

      assert (~is_nan r) by (destruct H2, r; easy).

      destruct x ; destruct b; destruct y ; destruct b;
        try (simpl in H; contradict H; now auto);
        try (destruct m; simpl in r; easy);
        simpl in h;
        destruct m; try (rewrite is_positive_Bsign; auto);
          rewrite is_negative_Bsign; auto.

    + destruct H4.
      unfold binary_overflow in H4.
      change (Bplus sb emax Hsb' Hemax' nan_bf m x y) with r in H4.
      destruct H2 as [H2|H2]; rewrite H2 in H4; simpl in H4;
        destruct overflow_to_inf in H4; easy.

    + apply Rnot_lt_le; assumption.
Qed.

Lemma no_overflow_or_not: forall m x, no_overflow m x \/ ~ no_overflow m x.
Proof.
  intros m x.
  rewrite no_overflow_Rabs_round_emax.
  destruct (Rlt_dec (Rabs (round m x)) (bpow radix2 emax));[left|right]; assumption.
Qed.

Lemma add_finite_rev_n' : forall (m:mode) (x:t) (y:t),
    is_finite (add m x y) ->
    (no_overflow m ((to_real x) + (to_real y))%R
     /\ to_real (add m x y) = round m ((to_real x) + (to_real y))%R)
    \/ to_real (add m x y) = max_real \/ to_real (add m x y) =-  max_real .
Proof.
intros m x y h1.
destruct (add_finite_rev m x y h1).

destruct (no_overflow_or_not m (to_real x + to_real y));[left|right].

split; [auto|apply add_finite; easy].
destruct (add_special m x y) as (_,(_,(_,(_,(_,(h,_)))))).
assert (is_finite x /\ is_finite y /\ ~ no_overflow m (to_real x + to_real y)) by auto.
apply h in H2; clear h.
destruct H2.
destruct (add m x y); destruct b, m; simpl in *; try easy;
  try (destruct H3; destruct H4; now auto);
  destruct H3, H3; auto.
Qed.

(* Why3 goal *)
Lemma sub_special : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  let r := (sub m x y) in ((((is_nan x) \/ (is_nan y)) -> (is_nan r)) /\
  ((((is_finite x) /\ (is_infinite y)) -> ((is_infinite r) /\ (diff_sign r
  y))) /\ ((((is_infinite x) /\ (is_finite y)) -> ((is_infinite r) /\
  (same_sign r x))) /\ ((((is_infinite x) /\ ((is_infinite y) /\ (same_sign x
  y))) -> (is_nan r)) /\ ((((is_infinite x) /\ ((is_infinite y) /\ (diff_sign
  x y))) -> ((is_infinite r) /\ (same_sign r x))) /\ ((((is_finite x) /\
  ((is_finite y) /\ ~ (no_overflow m ((to_real x) - (to_real y))%R))) ->
  ((same_sign_real r ((to_real x) - (to_real y))%R) /\ (overflow_value m
  r))) /\ (((is_finite x) /\ (is_finite y)) -> (((diff_sign x y) ->
  (same_sign r x)) /\ ((~ (diff_sign x y)) -> (sign_zero_result m
  r)))))))))).
Proof.
  intros m x y r.
  unfold same_sign, diff_sign, same_sign, same_sign_real.
  split;[intro h|split;[intros (h,h1)|split;[intros (h,h1)|split;[intros (h,(h1,h2))|split;[intros (h,(h1,h2))|split;[intros (h,(h1,h2))|split;[intro h|intro h]]]]]]].
  - destruct x, y; destruct b, b0; destruct h; easy.
  - destruct x, y; destruct b, b0; auto; easy.
  - destruct x, y; destruct b, b0; auto; easy.
  - destruct x, y; destruct b, b0; destruct h2 as [(h2,h3)|(h2,h3)]; auto; easy.
  - destruct x, y; destruct b, b0; destruct h2 as [(h2,h3)|(h2,h3)]; auto; easy.
  - rewrite no_overflow_Rabs_round_max_real, Rabs_round_max_real_emax in h2.
    apply Rnot_lt_le in h2.
    pose proof (Bminus_correct sb emax Hsb' Hemax' nan_bf m x y h h1).
    rewrite Rlt_bool_false in H by auto.
    destruct H.
    split.

    + destruct x, y; try easy.
      * destruct b, b0, m; simpl in H; easy.
      * rewrite B754_zero_to_real at 1 2.
        rewrite Rminus_0_l.
        rewrite <-(@B754_zero_to_real false) at 1 2.
        destruct (neg_finite (B754_finite b0 m0 e e0)) as (_,h3); auto.
        rewrite <-h3.
        destruct b0;[left;split;[easy|]|right;split;[easy|]]; apply lt_finite; easy.
      * rewrite B754_zero_to_real at 1 2.
        rewrite Rminus_0_r.
        rewrite <-(@B754_zero_to_real false) at 1 2.
        destruct b;[right;split;[easy|]|left;split;[easy|]]; apply lt_finite; easy.
      * change (Bminus sb emax Hsb' Hemax' nan_bf  m (B754_finite b m0 e e0) (B754_finite b0 m1 e1 e2)) with r in H.
        pose proof (sign_FF_overflow m (Bsign sb emax (B754_finite b m0 e e0))).
        rewrite <-H in H1.
        rewrite sign_FF_B2FF in H1.
        simpl Bsign at 2 in H1.
        assert (~is_nan r).
        { simpl binary_overflow in H.
          unfold binary_overflow in H.
          destruct overflow_to_inf in H;
            destruct r; try easy;
              destruct n; easy. }

        simpl in H0.
        apply Bool.negb_sym in H0. {

        destruct b; simpl in H0;rewrite H0 in *;[right|left];split.

        - rewrite <-is_negative_Bsign in H1; auto.
        - assert (to_real (B754_finite true m0 e e0) < 0) by
              (apply non_zero_negative_to_real; easy).
          assert (0 < to_real (B754_finite false m1 e1 e2)) by
              (apply non_zero_positive_to_real; easy).
          fourier.
        - rewrite <-is_positive_Bsign in H1; auto.
        - assert (0 < to_real (B754_finite false m0 e e0)) by
              (apply non_zero_positive_to_real; easy).
          assert (to_real (B754_finite true m1 e1 e2) < 0) by
              (apply non_zero_negative_to_real; easy).
          fourier. }

    + change (Bminus sb emax Hsb' Hemax' nan_bf m x y) with r in H.
      assert (H':=H).
      apply (f_equal sign_FF) in H'.
      rewrite sign_FF_B2FF, sign_FF_overflow in H'.
      destruct m; simpl;
        unfold binary_overflow in H;
        simpl in H.
      * destruct r; try easy; destruct n; easy.
      * destruct r; try easy; destruct n; easy.
      * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
            (destruct x ; destruct b; simpl; auto). {
        destruct H1; rewrite H1 in H', H0, H; simpl in H.
        - split.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H'; easy.
          intro; split.
          destruct r; try easy; destruct n; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H.
          + unfold to_real. rewrite <-min_real_is_F2R, <-FF2R_B2FF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            apply Pos.pow_gt_1.
            zify; auto with zarith.
        - split.
          destruct r; easy.
          intro.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign in H2; auto; easy. }
      * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
            (destruct x ; destruct b; simpl; auto). {
        destruct H1; rewrite H1 in H', H0, H; simpl in H.
        - split.
          intro.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign in H2; auto. rewrite H' in H2; easy.
          destruct r; try easy; destruct n; easy.
        - split.
          intro; split.
          destruct r; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H.
          + unfold to_real. rewrite <-max_real_is_F2R, <-FF2R_B2FF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
              apply Pos.pow_gt_1.
              zify; auto with zarith.
          + assert (~is_nan r) by
                (destruct r; try easy; destruct n; easy).
            rewrite is_positive_Bsign; easy. }
      * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
            (destruct x ; destruct b; simpl; auto).
        assert (~is_nan r) by
            (destruct H1, r; try easy; destruct n; easy).
        rewrite is_positive_Bsign; auto. {
        destruct H1; rewrite H1 in H', H0, H; simpl in H.
        - split.
          rewrite H'; easy.
          intro; split.
          destruct r; try easy; destruct n; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H.
          + unfold to_real. rewrite <-min_real_is_F2R, <-FF2R_B2FF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            apply Pos.pow_gt_1.
            zify; auto with zarith.
        - split.
          + intro; split.
            destruct r; try easy; destruct n; easy.
            replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H.
            * unfold to_real. rewrite <-max_real_is_F2R, <-FF2R_B2FF, H; auto.
            *  rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
               apply Pos.pow_gt_1.
               zify; auto with zarith.
          + easy. }
  - destruct H.
    pose proof (Bminus_correct sb emax Hsb' Hemax' nan_bf m x y H H0).
    destruct (Rlt_le_dec (Rabs (round m (to_real x - to_real y))) (bpow radix2 emax)).
    + rewrite Rlt_bool_true in H1; auto.
      destruct H1 as (h1,(h2,h3)).
      change (Bminus sb emax Hsb' Hemax' nan_bf m x y) with r in h1, h2, h3.
      assert (~is_nan r) by (destruct r; easy).
      destruct h as [(h,h')|(h,h')];[left|right];split;auto.
      * rewrite is_positive_Bsign; auto.
        destruct y; destruct b,x; destruct b; try easy.
        rewrite Rcompare_Gt in h3; auto.
        assert (B2R sb emax (B754_finite true m0 e e0) < 0) by
            (apply non_zero_negative_to_real; easy).
        assert (0 < B2R sb emax (B754_finite false m1 e1 e2)) by
            (apply non_zero_positive_to_real; easy).
        fourier.
      * rewrite is_negative_Bsign; auto.
        destruct y; destruct b,x; destruct b; try easy.
        rewrite Rcompare_Lt in h3; auto.
        assert (0 < B2R sb emax (B754_finite false m0 e e0)) by
            (apply non_zero_positive_to_real; easy).
        assert (B2R sb emax (B754_finite true m1 e1 e2) < 0) by
            (apply non_zero_negative_to_real; easy).
        fourier.
    + rewrite Rlt_bool_false in H1; auto.
      destruct H1 as (h1,h2).
      change (Bminus sb emax Hsb' Hemax' nan_bf m x y) with r in h1.
      destruct (is_nan_dec r).
      destruct x; destruct b,y; destruct b; try easy; destruct m;
        unfold binary_overflow in h1; simpl in h1;
          destruct r; try easy; destruct n; easy.

      rewrite is_positive_Bsign; auto.
      rewrite is_negative_Bsign; auto.
      apply (f_equal sign_FF) in h1.
      rewrite sign_FF_B2FF, sign_FF_overflow in h1.
      assert (~is_nan x) by (destruct x; easy).
      assert (~is_nan y) by (destruct y; easy).
      rewrite is_positive_Bsign in h,h; auto.
      rewrite is_negative_Bsign in h,h; auto.
      destruct h as [(h,h')|(h,h')];rewrite h in h1, h2;[left|right];split;auto.
      rewrite is_positive_Bsign; auto.
      rewrite is_negative_Bsign; auto.
  - intuition.
    unfold sign_zero_result; intro.
    unfold is_zero in H2.
    rewrite eq_zero_iff in H2.
    pose proof (Bminus_correct sb emax Hsb' Hemax' nan_bf m x y H0 H1).
    destruct (Rlt_dec (Rabs (round m (to_real x - to_real y))) (bpow radix2 emax)) as [r0|r0];
      [rewrite Rlt_bool_true in H4; auto; clear r0|
       rewrite Rlt_bool_false in H4].
    + destruct H4 as (h1,(h2,h)).

      assert (to_real x - to_real y = 0).
      { apply (round_plus_eq_zero radix2 fexp (round_mode m)).
        apply generic_format_B2R.
        destruct (neg_finite y) as (_,h3); auto; rewrite <-h3.
        apply generic_format_B2R.
        destruct H2 as [H2|H2]; apply (f_equal to_real) in H2.
        rewrite zeroF_to_real in H2.
        rewrite <-H2; auto.
        assert (is_finite zeroF) as zero_is_finite by easy.
        destruct (neg_finite zeroF zero_is_finite).
        rewrite H5, zeroF_to_real, Ropp_0 in H2.
        rewrite <-H2; auto. }

      rewrite Rcompare_Eq in h; auto.
      change (Bminus sb emax Hsb' Hemax' nan_bf m x y) with r in h.

      assert (~is_nan r) by (destruct H2, r; easy).

      destruct x ; destruct b; destruct y ; destruct b;
        try (simpl in H; contradict H; now auto);
        try (destruct m; simpl in r; easy);
        simpl in h;
        destruct m; try (rewrite is_positive_Bsign; auto);
          rewrite is_negative_Bsign; auto.

    + destruct H4.
      unfold binary_overflow in H4.
      change (Bminus sb emax Hsb' Hemax' nan_bf m x y) with r in H4.
      destruct H2 as [H2|H2]; rewrite H2 in H4; simpl in H4;
        destruct overflow_to_inf in H4; easy.

    + apply Rnot_lt_le; assumption.
Qed.

Lemma sub_finite_rev_n' : forall (m:mode) (x:t) (y:t),
    is_finite (sub m x y) ->
    (no_overflow m ((to_real x) - (to_real y))%R
     /\ to_real (sub m x y) = round m ((to_real x) - (to_real y))%R)
    \/ to_real (sub m x y) = max_real \/ to_real (sub m x y) =-  max_real .
Proof.
intros m x y h1.
destruct (sub_finite_rev m x y h1).
destruct (no_overflow_or_not m (to_real x - to_real y));[left|right].
split; [auto|apply sub_finite; easy].
destruct (sub_special m x y) as (_,(_,(_,(_,(_,(h,_)))))).
assert (is_finite x /\ is_finite y /\ ~ no_overflow m (to_real x - to_real y)) by auto.
apply h in H2; clear h.
destruct H2.
destruct (sub m x y); destruct b, m; simpl in *; try easy;
  try (destruct H3; destruct H4; now auto);
  destruct H3, H3; auto.
Qed.

(* Why3 goal *)
Lemma mul_special : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  let r := (mul m x y) in ((((is_nan x) \/ (is_nan y)) -> (is_nan r)) /\
  ((((is_zero x) /\ (is_infinite y)) -> (is_nan r)) /\ ((((is_finite x) /\
  ((is_infinite y) /\ ~ (is_zero x))) -> (is_infinite r)) /\ ((((is_infinite
  x) /\ (is_zero y)) -> (is_nan r)) /\ ((((is_infinite x) /\ ((is_finite
  y) /\ ~ (is_zero y))) -> (is_infinite r)) /\ ((((is_infinite x) /\
  (is_infinite y)) -> (is_infinite r)) /\ ((((is_finite x) /\ ((is_finite
  y) /\ ~ (no_overflow m ((to_real x) * (to_real y))%R))) -> (overflow_value
  m r)) /\ ((~ (is_nan r)) -> (product_sign r x y))))))))).
Proof.
  intros m x y r.
  unfold product_sign, same_sign, diff_sign.
  intuition.
  - destruct x; easy.
  - destruct x, y; easy.
  - destruct x, y; destruct b; easy.
  - destruct x, y; destruct b; try easy; contradict H2; easy.
  - destruct x, y; destruct b0; easy.
  - destruct x, y; destruct b0; try easy; contradict H2; easy.
  - destruct x, y; easy.
  - rewrite no_overflow_Rabs_round_max_real, Rabs_round_max_real_emax in H2.
    apply Rnot_lt_le in H2.
    pose proof (Bmult_correct sb emax Hsb' Hemax' nan_bf m x y).
    rewrite Rlt_bool_false in H1 by auto.
    change (Bmult sb emax Hsb' Hemax' nan_bf m x y) with r in H1.
    assert (H1':=H1).
    apply (f_equal sign_FF) in H1'.
    rewrite sign_FF_B2FF, sign_FF_overflow in H1'.
    destruct m; simpl;
      unfold binary_overflow in H1;
      simpl in H1.
    * destruct r; try easy; destruct n; easy.
    * destruct r; try easy; destruct n; easy.
    * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
          (destruct x ; destruct b; simpl; auto).
      assert (Bsign sb emax y = true \/ Bsign sb emax y = false) by
          (destruct y; destruct b; simpl; auto). {
        destruct H3, H4; rewrite H3, H4 in H1', H1; simpl in H1, H1'.
        - split.
          destruct r; easy.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
        - split.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
          intro; split.
          destruct r; try easy; destruct n; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H1.
          + unfold to_real. rewrite <-min_real_is_F2R, <-FF2R_B2FF, H1; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            apply Pos.pow_gt_1.
            zify; auto with zarith.
        - split.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
          intro; split.
          destruct r; try easy; destruct n; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H1.
          + unfold to_real. rewrite <-min_real_is_F2R, <-FF2R_B2FF, H1; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            apply Pos.pow_gt_1.
            zify; auto with zarith.
        - split.
          destruct r; easy.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H1'; intro h; contradict h; easy. }
    * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
          (destruct x ; destruct b; simpl; auto).
      assert (Bsign sb emax y = true \/ Bsign sb emax y = false) by
          (destruct y; destruct b; simpl; auto). {
      destruct H3, H4; rewrite H3, H4 in H1', H1; simpl in H1, H1'.
      - split.
        { intro; split.
          destruct r; try easy; destruct n; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H1.
          + unfold to_real. rewrite <-max_real_is_F2R, <-FF2R_B2FF, H1; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            apply Pos.pow_gt_1.
            zify; auto with zarith. }
        assert (~is_nan r) by
            (destruct r; try easy; destruct n; easy).
        rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
      - split.
        assert (~is_nan r) by
            (destruct r; try easy; destruct n; easy).
        rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
        destruct r; try easy; destruct n; easy.
      - split.
        assert (~is_nan r) by
            (destruct r; try easy; destruct n; easy).
        rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
        destruct r; try easy; destruct n; easy.
      - split.
        { intro; split.
          destruct r; try easy; destruct n; easy.
          replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H1.
          + unfold to_real. rewrite <-max_real_is_F2R, <-FF2R_B2FF, H1; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            apply Pos.pow_gt_1.
            zify; auto with zarith. }
        assert (~is_nan r) by
            (destruct r; try easy; destruct n; easy).
        rewrite is_positive_Bsign, H1'; intro h; contradict h; easy. }
    * assert (Bsign sb emax x = true \/ Bsign sb emax x = false) by
          (destruct x ; destruct b; simpl; auto).
      assert (Bsign sb emax y = true \/ Bsign sb emax y = false) by
          (destruct y; destruct b; simpl; auto).
      replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H1.
      { unfold to_real. rewrite <-min_real_is_F2R,<-max_real_is_F2R, <-FF2R_B2FF, H1; auto.
        destruct H3, H4; rewrite H3, H4 in *; simpl in *.
        - split.
          intro; split; [destruct r; easy|auto].
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
        - split.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
          intro; split; [destruct r; try easy; destruct n; easy|auto].
        - split.
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H1'; intro h; contradict h; easy.
          intro; split; [destruct r; try easy; destruct n; easy|auto].
        - split.
          intro; split; [destruct r; easy|auto].
          assert (~is_nan r) by
              (destruct r; try easy; destruct n; easy).
          rewrite is_positive_Bsign, H1'; intro h; contradict h; easy. }
      rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
      apply Pos.pow_gt_1.
      zify; auto with zarith.
  - pose proof (Bmult_correct sb emax Hsb' Hemax' nan_bf m x y).
    destruct (Rlt_le_dec (Rabs (round m (to_real x * to_real y))) (bpow radix2 emax));
    [rewrite Rlt_bool_true in H1; auto| rewrite Rlt_bool_false in H1; auto].
    + destruct H1 as (h1, (h2, h3)).
      rewrite is_positive_Bsign; auto.
      unfold r, mul, Hsb''.
      rewrite h3.
      destruct x; destruct b,y; destruct b; easy.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_FF) in H1.
      rewrite sign_FF_B2FF, sign_FF_overflow in H1.
      rewrite is_positive_Bsign; auto.
      destruct x; destruct b,y; destruct b; easy.
  - pose proof (Bmult_correct sb emax Hsb' Hemax' nan_bf m x y).
    destruct (Rlt_le_dec (Rabs (round m (to_real x * to_real y))) (bpow radix2 emax));
    [rewrite Rlt_bool_true in H1; auto| rewrite Rlt_bool_false in H1; auto].
    + destruct H1 as (h1, (h2, h3)).
      rewrite is_positive_Bsign; auto.
      unfold r, mul, Hsb''.
      rewrite h3.
      destruct x; destruct b,y; destruct b; easy.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_FF) in H1.
      rewrite sign_FF_B2FF, sign_FF_overflow in H1.
      rewrite is_positive_Bsign; auto.
      destruct x; destruct b,y; destruct b; easy.
  - pose proof (Bmult_correct sb emax Hsb' Hemax' nan_bf m x y).
    destruct (Rlt_le_dec (Rabs (round m (to_real x * to_real y))) (bpow radix2 emax));
    [rewrite Rlt_bool_true in H1; auto| rewrite Rlt_bool_false in H1; auto].
    + destruct H1 as (h1, (h2, h3)).
      rewrite is_negative_Bsign; auto.
      unfold r, mul, Hsb''.
      rewrite h3.
      destruct x; destruct b,y; destruct b; auto.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_FF) in H1.
      rewrite sign_FF_B2FF, sign_FF_overflow in H1.
      rewrite is_negative_Bsign; auto.
      destruct x; destruct b,y; destruct b; auto.
  - pose proof (Bmult_correct sb emax Hsb' Hemax' nan_bf m x y).
    destruct (Rlt_le_dec (Rabs (round m (to_real x * to_real y))) (bpow radix2 emax));
    [rewrite Rlt_bool_true in H1; auto| rewrite Rlt_bool_false in H1; auto].
    + destruct H1 as (h1, (h2, h3)).
      rewrite is_negative_Bsign; auto.
      unfold r, mul, Hsb''.
      rewrite h3.
      destruct x; destruct b,y; destruct b; auto.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_FF) in H1.
      rewrite sign_FF_B2FF, sign_FF_overflow in H1.
      rewrite is_negative_Bsign; auto.
      destruct x; destruct b,y; destruct b; auto.
Qed.

Lemma mul_finite_rev_n' : forall (m:mode) (x:t) (y:t),
    is_finite (mul m x y) ->
    (no_overflow m ((to_real x) * (to_real y))%R
     /\ to_real (mul m x y) = round m ((to_real x) * (to_real y))%R)
    \/ to_real (mul m x y) = max_real \/ to_real (mul m x y) =-  max_real .
Proof.
intros m x y h1.
destruct (mul_finite_rev m x y h1).
destruct (no_overflow_or_not m (to_real x * to_real y));[left|right].
split; [auto|apply mul_finite; easy].
destruct (mul_special m x y) as (_,(_,(_,(_,(_,(_,(h,_))))))).
assert (is_finite x /\ is_finite y /\ ~ no_overflow m (to_real x * to_real y)) by auto.
apply h in H2; clear h.
destruct (mul m x y); destruct b, m; simpl in *; try easy;
  try (destruct H2; destruct H3; now auto);
  destruct H2, H2; auto.
Qed.

(* Why3 goal *)
Lemma div_special : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  let r := (div m x y) in ((((is_nan x) \/ (is_nan y)) -> (is_nan r)) /\
  ((((is_finite x) /\ (is_infinite y)) -> (is_zero r)) /\ ((((is_infinite
  x) /\ (is_finite y)) -> (is_infinite r)) /\ ((((is_infinite x) /\
  (is_infinite y)) -> (is_nan r)) /\ ((((is_finite x) /\ ((is_finite y) /\
  ((~ (is_zero y)) /\ ~ (no_overflow m ((to_real x) / (to_real y))%R)))) ->
  (overflow_value m r)) /\ ((((is_finite x) /\ ((is_zero y) /\ ~ (is_zero
  x))) -> (is_infinite r)) /\ ((((is_zero x) /\ (is_zero y)) -> (is_nan
  r)) /\ ((~ (is_nan r)) -> (product_sign r x y))))))))).
Proof.
  intros m x y r.
  unfold product_sign, same_sign, diff_sign.
  intuition.
  - destruct x; easy.
  - destruct x, y; easy.
  - destruct x, y; destruct b; easy.
  - destruct x, y; destruct b; try easy; contradict H2; easy.
  - destruct x, y; destruct b0; easy.
  - assert (to_real y <> 0) by (rewrite zero_to_real in H1; auto).
    pose proof (Bdiv_correct sb emax Hsb' Hemax' nan_bf m x y H2).
    rewrite Rlt_bool_false in H4.
    + unfold binary_overflow in H4.
      change (Bdiv sb emax Hsb' Hemax' nan_bf m x y) with r in H4; auto.
      destruct m; simpl in *.
      * destruct r; try easy.
        destruct b, n in H4; easy.
      * destruct r; try easy.
        destruct b, n in H4; easy.
      * destruct (xorb (Bsign sb emax x) (Bsign sb emax y)); simpl in H4. {
          split; intro.
          - destruct r; destruct b; easy.
          - split; [destruct r; try easy; destruct b, n in H4; easy|].
            apply (f_equal (FF2R radix2)) in H4.
            rewrite FF2R_B2FF in H4.
            simpl in H4.
            replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H4 by
                (rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto;
                 apply Pos.pow_gt_1;
                 zify; auto with zarith).
            rewrite <-min_real_is_F2R; assumption. }
        split; intro; [destruct r; easy|].
        destruct r; try easy.
        destruct b; try easy.
        simpl in H5; contradict H5; auto.
        destruct n; easy.
      * destruct (xorb (Bsign sb emax x) (Bsign sb emax y)); simpl in H4. {
        split; intro.
        - destruct r; destruct b; easy.
        - destruct r; try easy.
           destruct n; easy. }
        { split; intro.
          + split;[destruct r; easy|].
            apply (f_equal (FF2R radix2)) in H4.
            rewrite FF2R_B2FF in H4.
            simpl in H4.
            replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H4 by
                (rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto;
                 apply Pos.pow_gt_1;
                 zify; auto with zarith).
            rewrite <-max_real_is_F2R; assumption.
          + destruct r; try easy; try (destruct n; easy).
            destruct b; try easy.
            simpl in H5; contradict H5; auto. }
      * { destruct (xorb (Bsign sb emax x) (Bsign sb emax y)); simpl in H4;
        split; intro.
          - destruct r; destruct b; easy.
          - split;[destruct r; destruct b; try easy; destruct n; easy|].
            apply (f_equal (FF2R radix2)) in H4.
            rewrite FF2R_B2FF in H4.
            simpl in H4.
            replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H4 by
                (rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto;
                 apply Pos.pow_gt_1;
                 zify; auto with zarith).
            rewrite <-min_real_is_F2R; assumption.
          - split; [destruct r; try easy| ].
            apply (f_equal (FF2R radix2)) in H4.
            rewrite FF2R_B2FF in H4.
            simpl in H4.
            replace (Z.pow_pos 2 sb_pos - 1)%Z with (Z.pos (2 ^ sb_pos - 1)) in H4 by
                (rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto;
                 apply Pos.pow_gt_1;
                 zify; auto with zarith).
            rewrite <-max_real_is_F2R; assumption.
          - contradict H5.
            destruct r; destruct b; try easy; destruct n; easy. }
    + clear H4.
      rewrite no_overflow_Rabs_round_emax in H3.
      apply Rge_le, Rfourier_not_lt_ge; assumption.
  - destruct x, y; try easy.
    rewrite is_zero_B754_zero in H2; destruct H2; exists b; reflexivity.
    rewrite is_zero_B754_zero in H2; destruct H2; exists b; reflexivity.
    rewrite is_zero_B754_zero in H; destruct H; inversion H.
    rewrite is_zero_B754_zero in H; destruct H; inversion H.
  - rewrite is_zero_B754_zero in H0; destruct H0.
    rewrite is_zero_B754_zero in H1; destruct H1.
    destruct x, y; easy.
  - destruct x ; destruct b; destruct y ; destruct b; try easy.
    now elim H.
    now elim H.
    set (x:=B754_finite false m0 e e0);
      set (y:=B754_finite false m1 e1 e2); fold x y in r, H0, H2.
    assert (to_real y <> 0).
    { assert (0 < to_real y) by
          (apply non_zero_positive_to_real; easy).
      apply not_eq_sym, Rlt_not_eq; fourier. }
    pose proof (Bdiv_correct sb emax Hsb' Hemax' nan_bf m x y H1).
    destruct (Rlt_le_dec (Rabs (round m (to_real x / to_real y))) (bpow radix2 emax));
      [rewrite Rlt_bool_true in H3|rewrite Rlt_bool_false in H3];auto.
    + destruct H3 as (_,(_,h)).
      rewrite is_positive_Bsign; auto.
      unfold r, div, Hsb''.
      rewrite h.
      easy.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_FF) in H3.
      rewrite sign_FF_B2FF, sign_FF_overflow in H3.
      rewrite is_positive_Bsign; auto.
  - destruct x ; destruct b; destruct y ; destruct b; try easy.
    now elim H.
    now elim H.
    set (x:=B754_finite true m0 e e0);
      set (y:=B754_finite true m1 e1 e2); fold x y in r, H0, H2.
    assert (to_real y <> 0).
    { assert (to_real y < 0) by
          (apply non_zero_negative_to_real; easy).
      apply Rlt_not_eq; fourier. }
    pose proof (Bdiv_correct sb emax Hsb' Hemax' nan_bf m x y H1).
    destruct (Rlt_le_dec (Rabs (round m (to_real x / to_real y))) (bpow radix2 emax));
      [rewrite Rlt_bool_true in H3|rewrite Rlt_bool_false in H3];auto.
    + destruct H3 as (_,(_,h)).
      rewrite is_positive_Bsign; auto.
      unfold r, div, Hsb''.
      rewrite h.
      easy.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_FF) in H3.
      rewrite sign_FF_B2FF, sign_FF_overflow in H3.
      rewrite is_positive_Bsign; auto.
  - destruct x ; destruct b; destruct y ; destruct b; try easy.
    now elim H.
    now elim H.
    set (x:=B754_finite false m0 e e0);
      set (y:=B754_finite true m1 e1 e2); fold x y in r, H0, H2.
    assert (to_real y <> 0).
    { assert (to_real y < 0) by
          (apply non_zero_negative_to_real; easy).
      apply Rlt_not_eq; fourier. }
    pose proof (Bdiv_correct sb emax Hsb' Hemax' nan_bf m x y H1).
    destruct (Rlt_le_dec (Rabs (round m (to_real x / to_real y))) (bpow radix2 emax));
      [rewrite Rlt_bool_true in H3|rewrite Rlt_bool_false in H3];auto.
    + destruct H3 as (_,(_,h)).
      rewrite is_negative_Bsign; auto.
      unfold r, div, Hsb''.
      rewrite h.
      easy.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_FF) in H3.
      rewrite sign_FF_B2FF, sign_FF_overflow in H3.
      rewrite is_negative_Bsign; auto.
  - destruct x ; destruct b; destruct y ; destruct b; try easy.
    now elim H.
    now elim H.
    set (x:=B754_finite true m0 e e0);
      set (y:=B754_finite false m1 e1 e2); fold x y in r, H0, H2.
    assert (to_real y <> 0).
    { assert (0 < to_real y) by
          (apply non_zero_positive_to_real; easy).
      apply not_eq_sym, Rlt_not_eq; fourier. }
    pose proof (Bdiv_correct sb emax Hsb' Hemax' nan_bf m x y H1).
    destruct (Rlt_le_dec (Rabs (round m (to_real x / to_real y))) (bpow radix2 emax));
      [rewrite Rlt_bool_true in H3|rewrite Rlt_bool_false in H3];auto.
    + destruct H3 as (_,(_,h)).
      rewrite is_negative_Bsign; auto.
      unfold r, div, Hsb''.
      rewrite h.
      easy.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_FF) in H3.
      rewrite sign_FF_B2FF, sign_FF_overflow in H3.
      rewrite is_negative_Bsign; auto.
Qed.

(* Why3 goal *)
Lemma neg_special : forall (x:t), ((is_nan x) -> (is_nan (neg x))) /\
  (((is_infinite x) -> (is_infinite (neg x))) /\ ((~ (is_nan x)) ->
  (diff_sign x (neg x)))).
Proof.
  intros x.
  split; [|split]; intro.
  - destruct x; easy.
  - destruct x; easy.
  - unfold diff_sign.
    destruct x.
    destruct b;[right|left]; easy.
    destruct b;[right|left]; easy.
    contradict H; easy.
    destruct b;[right|left]; easy.
Qed.

(* Why3 goal *)
Lemma abs_special : forall (x:t), ((is_nan x) -> (is_nan (abs x))) /\
  (((is_infinite x) -> (is_infinite (abs x))) /\ ((~ (is_nan x)) ->
  (is_positive (abs x)))).
Proof.
  intros x.
  split;[|split];intro.
  - destruct x; easy.
  - destruct x; easy.
  - destruct x; try easy.
    contradict H; easy.
Qed.

(* add to theory ? *)
Lemma abs_le_inv: forall {x y}, le (abs x) y -> le (neg y) x /\ le x y.
Proof.
  intros x y.
  destruct (Finite_Infinite_Nan_dec y) as [[hy|hy]|hy].
  + destruct (Finite_Infinite_Nan_dec x) as [[hx|hx]|hx].

    * pose proof (is_finite_abs _ hx).
      destruct (neg_finite _ hy).
      rewrite (le_to_real (abs x) y) by auto.
      rewrite (le_to_real (neg y) x) by auto.
      rewrite le_to_real by auto.
      rewrite H1 by auto.
      destruct (abs_finite _ hx) as (_,(u,_)).
      rewrite u.
      apply Rabs_le_inv.

    * intros a.
      pose proof (abs_special x) as (_,(b,_)); pose proof (b hx); clear b.
      destruct (le_special _ _ a) as [H1|[H1|H1]].
      - destruct x; easy.
      - unfold is_minus_infinity in H1.
        destruct H1, H1, x, y; try easy; destruct b0, b1; easy.
      - destruct y; unfold is_plus_infinity in H1; easy.

    * intros a.
      pose proof (abs_special x) as (b,_); pose proof (b hx); clear b.
      destruct (le_special _ _ a) as [H1|[H1|H1]];
        unfold is_minus_infinity, is_not_nan in H1;
        destruct (abs x), H1; try easy.
      destruct H0; easy.

  + intros a.

    destruct (Finite_Infinite_Nan_dec x) as [[hx|hx]|hx].
    * pose proof (is_finite_abs _ hx).
      destruct (le_special _ _ a) as [H1|[H1|H1]].
      - destruct y; easy.
      - unfold is_minus_infinity in H1; destruct x; easy.
      - destruct y, H1; try easy.
        unfold is_plus_infinity in H1; destruct b; try easy.
        destruct x ; destruct b; split; easy.
    * unfold Bcompare.
      destruct x, y; destruct b, b0; simpl; split; auto; easy.
    * destruct x; unfold le, Bcompare in a; try easy.
      destruct a as [a|a]; contradict a; easy.
  + intros a.
    destruct y; unfold le, Bcompare in a; try easy.
    destruct x; destruct b0; split; easy.
Qed.

(* Why3 goal *)
Lemma fma_special : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t)
  (z:t), let r := (fma m x y z) in ((((is_nan x) \/ ((is_nan y) \/ (is_nan
  z))) -> (is_nan r)) /\ ((((is_zero x) /\ (is_infinite y)) -> (is_nan r)) /\
  ((((is_infinite x) /\ (is_zero y)) -> (is_nan r)) /\ ((((is_finite x) /\
  ((~ (is_zero x)) /\ ((is_infinite y) /\ (is_finite z)))) -> ((is_infinite
  r) /\ (product_sign r x y))) /\ ((((is_finite x) /\ ((~ (is_zero x)) /\
  ((is_infinite y) /\ (is_infinite z)))) -> (((product_sign z x y) ->
  ((is_infinite r) /\ (same_sign r z))) /\ ((~ (product_sign z x y)) ->
  (is_nan r)))) /\ ((((is_infinite x) /\ ((is_finite y) /\ ((~ (is_zero
  y)) /\ (is_finite z)))) -> ((is_infinite r) /\ (product_sign r x y))) /\
  ((((is_infinite x) /\ ((is_finite y) /\ ((~ (is_zero y)) /\ (is_infinite
  z)))) -> (((product_sign z x y) -> ((is_infinite r) /\ (same_sign r z))) /\
  ((~ (product_sign z x y)) -> (is_nan r)))) /\ ((((is_infinite x) /\
  ((is_infinite y) /\ (is_finite z))) -> ((is_infinite r) /\ (product_sign r
  x y))) /\ ((((is_finite x) /\ ((is_finite y) /\ (is_infinite z))) ->
  ((is_infinite r) /\ (same_sign r z))) /\ ((((is_infinite x) /\
  ((is_infinite y) /\ (is_infinite z))) -> (((product_sign z x y) ->
  ((is_infinite r) /\ (same_sign r z))) /\ ((~ (product_sign z x y)) ->
  (is_nan r)))) /\ ((((is_finite x) /\ ((is_finite y) /\ ((is_finite z) /\
  ~ (no_overflow m (((to_real x) * (to_real y))%R + (to_real z))%R)))) ->
  ((same_sign_real r (((to_real x) * (to_real y))%R + (to_real z))%R) /\
  (overflow_value m r))) /\ (((is_finite x) /\ ((is_finite y) /\ (is_finite
  z))) -> (((product_sign z x y) -> (same_sign r z)) /\ ((~ (product_sign z x
  y)) -> (((((to_real x) * (to_real y))%R + (to_real z))%R = 0%R) ->
  (((m = ieee_float.RoundingMode.RTN) -> (is_negative r)) /\
  ((~ (m = ieee_float.RoundingMode.RTN)) -> (is_positive r)))))))))))))))))).
Proof.
intros m x y z r.
Admitted.

Lemma fma_finite_rev_n' : forall (m:mode) (x:t) (y:t) (z:t),
    is_finite (fma m x y z) ->
    (no_overflow m (to_real x * to_real y + to_real z)%R
     /\ to_real (fma m x y z) = round m (to_real x * to_real y + to_real z)%R)
    \/ to_real (fma m x y z) = max_real \/ to_real (fma m x y z) =-  max_real .
Proof.
intros m x y z h1.
destruct (fma_finite_rev m x y z h1) as (H,(H0,H1)).

destruct (no_overflow_or_not m (to_real x * to_real y + to_real z));[left|right].

split; [auto|apply fma_finite; easy].
destruct (fma_special m x y z) as (_,(_,(_,(_,(_,(_,(_,(_,(_,(_,(h,_))))))))))).
assert (is_finite x /\ is_finite y /\ is_finite z /\ ~ no_overflow m (to_real x * to_real y + to_real z)) by auto.
apply h in H3; clear h.
destruct (fma m x y z); destruct b, m; simpl in *; try easy;
  try (destruct H3; destruct H4; destruct H4; now auto);
  destruct H3; destruct H4; destruct H5; auto.
Qed.

(* Why3 goal *)
Lemma sqrt_special : forall (m:ieee_float.RoundingMode.mode) (x:t), let r :=
  (sqrt m x) in (((is_nan x) -> (is_nan r)) /\ (((is_plus_infinity x) ->
  (is_plus_infinity r)) /\ (((is_minus_infinity x) -> (is_nan r)) /\
  ((((is_finite x) /\ ((to_real x) < 0%R)%R) -> (is_nan r)) /\ (((is_zero
  x) -> (same_sign r x)) /\ (((is_finite x) /\ (0%R < (to_real x))%R) ->
  (is_positive r))))))).
Proof.
  intros m x r.
  unfold sqrt in r.
  intuition.
  - destruct x; easy.
  - unfold is_plus_infinity in *.
    destruct x ; destruct b; easy.
  - unfold is_minus_infinity in H.
    destruct x ; destruct b; easy.
  - destruct x ; destruct b; try easy.
    rewrite B754_zero_to_real in H1; fourier.
    rewrite B754_zero_to_real in H1; fourier.
    apply (to_real_negative _ H0) in H1.
    rewrite is_negative_Bsign in H1 by easy.
    easy.
  - unfold same_sign.
    rewrite is_zero_B754_zero in H; destruct H.
    destruct x; try easy.
    destruct b;[right|left];split;auto.
    simpl in r; unfold r; auto.
    simpl in r; unfold r; auto.
  - destruct (Bsqrt_correct sb emax Hsb' Hemax' (fun b => (true,One_Nan_pl)) m x) as (_,(h1,h2));
      fold r in h1, h2.
    destruct x; try easy.
    rewrite B754_zero_to_real in H1 at 1; fourier.
    apply (to_real_positive _ H0) in H1.
    rewrite is_positive_Bsign in H1 by easy.
    simpl in H1.
    destruct b; try easy.
    assert (not (is_nan r)) by (destruct r; easy).
    rewrite (is_positive_Bsign _ H).
    apply h2.
    now apply Bool.not_true_is_false.
Qed.

Lemma in_int_range_no_overflow : forall m {i}, in_int_range i -> no_overflow m (IZR i).
Proof.
  intros m i h.
  apply Bounded_real_no_overflow.
  unfold in_int_range in h.
  unfold in_range.
  rewrite max_real_int, <-FromInt.Neg, <-Z2R_IZR, <-Z2R_IZR, <-Z2R_IZR.
  pose proof pow2sb_lt_max_int.
  split; apply Z2R_le; auto with zarith.
Qed.

(* Why3 goal *)
Lemma of_int_add_exact : forall (m:ieee_float.RoundingMode.mode)
  (n:ieee_float.RoundingMode.mode) (i:Z) (j:Z), (in_safe_int_range i) ->
  ((in_safe_int_range j) -> ((in_safe_int_range (i + j)%Z) -> (eq (of_int m
  (i + j)%Z) (add n (of_int m i) (of_int m j))))).
Proof.
  intros m n i j h1 h2 h3.
  assert (h1':= in_safe_int_range_no_overflow m h1).
  assert (h2':= in_safe_int_range_no_overflow m h2).
  assert (h3':= in_safe_int_range_no_overflow n h3).
  assert (h3'':= in_safe_int_range_no_overflow m h3).
  assert (is_finite (of_int m i)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int m j)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int n (i+j)%Z)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int m (i+j)%Z)) by (apply of_int_correct; assumption).
  destruct (of_int_correct h1') as (f,_).
  destruct (of_int_correct h2') as (g,_).
  destruct (add_finite n (of_int m i) (of_int m j)); auto.
  simpl; rewrite f, g, Exact_rounding_for_integers, Exact_rounding_for_integers; auto.
  rewrite <-plus_IZR; assumption.
  destruct (of_int_correct h3'') as (h,_).
  rewrite to_real_eq, H4, f, g, h; auto.
  repeat rewrite Exact_rounding_for_integers; auto.
  rewrite <-plus_IZR, Exact_rounding_for_integers; auto; reflexivity.
Qed.

(* Why3 goal *)
Lemma of_int_sub_exact : forall (m:ieee_float.RoundingMode.mode)
  (n:ieee_float.RoundingMode.mode) (i:Z) (j:Z), (in_safe_int_range i) ->
  ((in_safe_int_range j) -> ((in_safe_int_range (i - j)%Z) -> (eq (of_int m
  (i - j)%Z) (sub n (of_int m i) (of_int m j))))).
Proof.
  intros m n i j h1 h2 h3.
  assert (h1':= in_safe_int_range_no_overflow m h1).
  assert (h2':= in_safe_int_range_no_overflow m h2).
  assert (h3':= in_safe_int_range_no_overflow n h3).
  assert (h3'':= in_safe_int_range_no_overflow m h3).
  assert (is_finite (of_int m i)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int m j)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int n (i-j)%Z)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int m (i-j)%Z)) by (apply of_int_correct; assumption).
  destruct (of_int_correct h1') as (f,_).
  destruct (of_int_correct h2') as (g,_).
  destruct (sub_finite n (of_int m i) (of_int m j)); auto.
  simpl; rewrite f, g, Exact_rounding_for_integers, Exact_rounding_for_integers; auto.
  rewrite <-minus_IZR; assumption.
  destruct (of_int_correct h3'') as (h,_).
  rewrite to_real_eq, H4, f, g, h; auto.
  repeat rewrite Exact_rounding_for_integers; auto.
  rewrite <-minus_IZR, Exact_rounding_for_integers; auto; reflexivity.
Qed.

(* Why3 goal *)
Lemma of_int_mul_exact : forall (m:ieee_float.RoundingMode.mode)
  (n:ieee_float.RoundingMode.mode) (i:Z) (j:Z), (in_safe_int_range i) ->
  ((in_safe_int_range j) -> ((in_safe_int_range (i * j)%Z) -> (eq (of_int m
  (i * j)%Z) (mul n (of_int m i) (of_int m j))))).
Proof.
  intros m n i j h1 h2 h3.
  assert (h1':= in_safe_int_range_no_overflow m h1).
  assert (h2':= in_safe_int_range_no_overflow m h2).
  assert (h3':= in_safe_int_range_no_overflow n h3).
  assert (h3'':= in_safe_int_range_no_overflow m h3).
  assert (is_finite (of_int m i)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int m j)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int n (i*j)%Z)) by (apply of_int_correct; assumption).
  assert (is_finite (of_int m (i*j)%Z)) by (apply of_int_correct; assumption).
  destruct (of_int_correct h1') as (f,_).
  destruct (of_int_correct h2') as (g,_).
  destruct (mul_finite n (of_int m i) (of_int m j)); auto.
  simpl; rewrite f, g,
         Exact_rounding_for_integers, Exact_rounding_for_integers; auto.
  rewrite <-mult_IZR; assumption.
  destruct (of_int_correct h3'') as (h,_).
  rewrite to_real_eq, H4, f, g, h; auto.
  repeat rewrite Exact_rounding_for_integers; auto.
  rewrite <-mult_IZR, Exact_rounding_for_integers; auto; reflexivity.
Qed.

(* Why3 goal *)
Lemma Min_r : forall (x:t) (y:t), (le y x) -> (eq (min x y) y).
Proof.
intros x y h1.
destruct h1;
pose (Bcompare_swap _ _ y x);
rewrite H in e;
unfold min; rewrite e; simpl.
apply (eq_not_nan_refl (proj1 (lt_not_nan H))).
apply (eq_not_nan_refl (proj1 (eq_not_nan H))).
Qed.

(* Why3 goal *)
Lemma Min_l : forall (x:t) (y:t), (le x y) -> (eq (min x y) x).
Proof.
intros x y h1.
destruct h1; unfold min; rewrite H; simpl.
apply (eq_not_nan_refl (proj1 (lt_not_nan H))).
pose (Bcompare_swap _ _ x y); rewrite H in e; apply e.
Qed.

(* Why3 goal *)
Lemma Max_r : forall (x:t) (y:t), (le y x) -> (eq (max x y) x).
Proof.
intros x y h1.
destruct h1;
pose (Bcompare_swap _ _ y x);
rewrite H in e;
unfold max; rewrite e; simpl.
apply (eq_not_nan_refl (proj2 (lt_not_nan H))).
apply (eq_not_nan_refl (proj2 (eq_not_nan H))).
Qed.

(* Why3 goal *)
Lemma Max_l : forall (x:t) (y:t), (le x y) -> (eq (max x y) y).
Proof.
intros x y h1.
destruct h1; unfold max; rewrite H; simpl.
apply (eq_not_nan_refl (proj2 (lt_not_nan H))).
apply H.
Qed.

Definition is_intR: R -> Prop.
Proof.
 exact (fun x => x = Z2R (Zfloor x)).
Defined.

Lemma is_intR_equiv: forall {x}, (exists i:int, x = Z2R i) -> is_intR x.
Proof.
  unfold is_intR.
  intros x h; destruct h.
  rewrite H, Zfloor_Z2R; reflexivity.
Qed.

Lemma is_intR_Z2R: forall i, is_intR (Z2R i).
Proof.
  intro i; apply is_intR_equiv; exists i; reflexivity.
Qed.

Lemma is_intR_FIX_format: forall {x}, is_intR x <-> FIX_format radix2 0%Z x.
Proof.
  intro x; unfold FIX_format; split; intro.
  exists ({| Fnum := Zfloor x; Fexp := 0 |}); simpl; split; auto.
  unfold F2R, Fnum, Fexp; simpl.
  rewrite Rmult_1_r; assumption.
  destruct H, H.
  unfold F2R in H.
  rewrite H0 in H; simpl in H.
  rewrite Rmult_1_r in H.
  apply is_intR_equiv.
  exists (Fnum x0); assumption.
Qed.

Lemma is_intR_round: forall {x m}, is_intR x -> is_intR (round m x).
Proof.
  intros x m h.
  rewrite is_intR_FIX_format.
  apply FIX_format_generic.
  apply generic_round_generic.
  apply FIX_exp_valid.
  apply fexp_Valid.
  apply valid_rnd_round_mode.
  apply generic_format_FIX.
  rewrite <-is_intR_FIX_format; assumption.
Qed.

(* Why3 goal *)
Definition is_int: t -> Prop.
Proof.
 exact (fun x => is_finite x /\ is_intR (to_real x)).
Defined.

Hint Unfold is_int.

Lemma is_int_or_not: forall (x:t), is_int x \/ ~ is_int x.
Proof.
  intro x.
  destruct x.
  - left.
    split.
    easy.
    rewrite B754_zero_to_real.
    unfold is_intR.
    change 0 with (Z2R 0%Z) at 2.
    rewrite Zfloor_Z2R; auto.
  - right; intro h; destruct h; easy.
  - right; intro h; destruct h; easy.
  - set (x := (B754_finite b m e e0)).
    unfold is_int, is_intR.
    destruct (Req_dec (to_real x) (Z2R (floor (to_real x)))).
    left.
    rewrite H, Zfloor_Z2R; easy.
    right.
    intro h; destruct h; auto.
Qed.

Lemma Bmax_rep_int_is_int: is_int Bmax_rep_int.
Proof.
  split. easy.
  rewrite Bmax_rep_int_to_real.
  rewrite <-Z2R_IZR; apply is_intR_Z2R.
Qed.

Lemma B754_zero_is_int : forall {b}, (is_int (B754_zero b)).
Proof.
  split. easy.
  rewrite B754_zero_to_real.
  unfold is_intR.
  change 0%R with (Z2R 0).
  now rewrite Zfloor_Z2R.
Qed.

Lemma max_value_is_int : is_int max_value.
Proof.
  split. easy.
  unfold is_intR.
  rewrite max_value_to_real, max_real_int.
  rewrite Floor_int.
  rewrite Z2R_IZR.
  reflexivity.
Qed.

(* TODO: add to theory *)
Lemma neg_is_int : forall {x}, is_int x -> is_int (neg x).
Proof.
  intros x (h,g).
  destruct (neg_finite _ h).
  split; auto.
  rewrite H0.
  rewrite g.
  unfold is_intR.
  rewrite <-Z2R_opp at 2.
  rewrite Zfloor_Z2R.
  symmetry; apply Z2R_opp.
Qed.

(* Why3 goal *)
Lemma zeroF_is_int : (is_int zeroF).
Proof.
  apply B754_zero_is_int.
Qed.

(* Why3 goal *)
Lemma of_int_is_int : forall (m:ieee_float.RoundingMode.mode) (x:Z),
  (in_int_range x) -> (is_int (of_int m x)).
Proof.
  intros m x (h1,h2).
  assert (no_overflow m (IZR x)) as h3.
  apply Bounded_real_no_overflow.
  unfold in_range.
  rewrite max_real_int.
  rewrite <-opp_IZR.
  split; apply IZR_le; assumption.
  destruct (of_int_correct h3) as (h4,(h5,_)).
  split; auto.
  rewrite h4.
  apply is_intR_round.
  rewrite <-Z2R_IZR.
  apply is_intR_Z2R.
Qed.

Lemma int_to_real_ : forall {m:mode} {x:t}, (is_int x) ->
  ((to_real x) = (BuiltIn.IZR (to_int m x))).
Proof.
intros m x h1.
destruct h1.
assert (is_intR (to_real x)) by assumption.
unfold is_intR in H0.
unfold to_int.
rewrite Znearest_imp with (n := (floor (to_real x))).
fold (to_real x).
case m; rewrite <-Z2R_IZR;
  [auto|
   destruct valid_rnd_NA|
   destruct valid_rnd_UP|
   destruct valid_rnd_DN|
   destruct valid_rnd_ZR]; rewrite H0;
rewrite Zrnd_Z2R; easy.
apply Rabs_lt.
rewrite Rminus_diag_eq.
split; fourier.
assumption.
Qed.

(* TODO: add to theory? *)
Lemma neg_int_to_int : forall {x} {m:mode}, is_int x -> to_int m (neg x) = (- (to_int m x))%Z.
Proof.
  intros x m h.
  apply eq_IZR.
  rewrite FromInt.Neg, <-(int_to_real_ h), <-(int_to_real_ (neg_is_int h)).
  destruct h.
  apply neg_finite; auto.
Qed.

Lemma Bmax_rep_int_to_int: forall {m}, to_int m Bmax_rep_int = pow2sb.
Proof.
  intro m.
  apply eq_IZR.
  rewrite <-int_to_real_.
  apply Bmax_rep_int_to_real.
  apply Bmax_rep_int_is_int.
Qed.

Lemma pow2sb_finite : forall (m:mode), is_finite (of_int m pow2sb).
Proof.
  intro.
  apply of_int_correct.
  apply Bounded_real_no_overflow.
  apply rep_int_in_range.
  split; auto with zarith.
  unfold pow2sb.
  assert (0 <= 2 ^ sb)%Z by (apply Z.pow_nonneg; auto with zarith).
  auto with zarith.
Qed.

Lemma Bmax_rep_int_of_int: forall {m:mode}, Bmax_rep_int = of_int m pow2sb.
Proof.
  intro m.
  pose proof pow2sb_finite.
  apply feq_eq; try easy.
  rewrite to_real_eq; try easy.

  assert (- pow2sb <= pow2sb <= pow2sb)%Z.
  split; auto with zarith.
  assert (0 < pow2sb)%Z.
  apply (Z.pow_pos_nonneg 2 sb); auto with zarith.
  apply Z.lt_le_incl, Hsb'.
  auto with zarith.

  destruct (@of_int_correct m pow2sb) as (f,_); auto.
  apply Bounded_real_no_overflow.
  apply rep_int_in_range; auto.

  rewrite f, Bmax_rep_int_to_real.
  symmetry.
  apply Exact_rounding_for_integers; auto.
Qed.

(* Why3 goal *)
Lemma big_float_is_int : forall (m:ieee_float.RoundingMode.mode) (i:t),
  (is_finite i) -> (((le i (neg (of_int m pow2sb))) \/ (le (of_int m pow2sb)
  i)) -> (is_int i)).
Proof.
  intros m i h1 h2.
  destruct i; try easy.
  apply B754_zero_is_int.
  split; auto.
  rewrite <-Bmax_rep_int_of_int in h2.
  unfold to_real, B2R, F2R,Fnum,Fexp.

  assert (1 <= e)%Z.
  { unfold le in h2; simpl Bcompare in h2.
    destruct b.
    destruct (Z_lt_le_dec e 1%Z); auto.
    rewrite Zcompare_Lt in h2; auto.
    destruct h2 as [[h2|h2]|[h2|h2]]; contradict h2; easy.
    destruct h2 as [[h2|h2]|h2]; try (contradict h2; easy).
    destruct e.
    destruct h2 as [h2|h2]; contradict h2; easy.
    pose proof (Pos2Z.is_pos p).
    auto with zarith.
    destruct h2 as [h2|h2]; contradict h2; easy. }

  rewrite <-Z2R_Zpower by auto with zarith.
  rewrite <-Z2R_mult.
  apply is_intR_Z2R.
Qed.

Lemma max_value_to_int : forall m, to_int m max_value = max_int.
Proof.
  intro m.
  apply eq_IZR.
  rewrite <-max_real_int, <-int_to_real_, max_value_to_real.
  reflexivity.
  unfold is_int.

  apply max_value_is_int.
Qed.

Lemma neg_to_int_max_value : forall {m}, (- to_int m max_value)%Z = to_int m (neg max_value).
Proof.
  intro m.
  destruct (valid_rnd_round_mode m).
  pose proof max_value_is_int as H.
  pose proof (neg_is_int H).
  apply eq_IZR.
  rewrite Ropp_Ropp_IZR.
  rewrite <-int_to_real_, <-int_to_real_  by auto.
  now destruct (neg_finite max_value) as (_,h).
Qed.

Lemma is_finite_range_to_int : forall {x} m, (is_finite x) -> (in_range (IZR (to_int m x))).
Proof.
  intros x m h1.
  apply Rabs_le_inv.
  rewrite Abs.Abs_le, max_real_int, <-opp_IZR, <-(max_value_to_int m), neg_to_int_max_value.

  pose proof (bounded_floats_le _ h1).
  pose proof (abs_le_inv H) as (H1,H2).
  now split; apply IZR_le; apply to_int_le.
Qed.

Lemma is_finite_to_int: forall {x} (m1 m2:mode), is_finite x -> no_overflow m1 (IZR (to_int m2 x)).
Proof.
  intros x m1 m2 h;
  apply (Bounded_real_no_overflow m1 _ (is_finite_range_to_int m2 h)).
Qed.

Lemma is_finite_to_int2: forall {x} m, is_finite x -> (- max_int <= to_int m x <= max_int)%Z.
Proof.
  intros x m h.
  rewrite <-(@max_value_to_int m).
  rewrite (@neg_to_int_max_value m).
  pose proof (bounded_floats_le _ h).
  apply abs_le_inv in H.
  destruct H.
  now split; apply to_int_le.
Qed.

Lemma roundToIntegral_finite: forall m {x}, is_finite x -> is_finite (roundToIntegral m x).
Proof.
  intros m x h; destruct x; auto.
  unfold roundToIntegral.
  destruct Z.eq_dec; auto.
  apply of_int_correct.
  apply (is_finite_to_int RTZ m h).
Qed.

(* Why3 goal *)
Lemma roundToIntegral_is_int : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (is_finite x) -> (is_int (roundToIntegral m x)).
Proof.
  intros m x h1.
  destruct x; try easy.
  + apply zeroF_is_int.
  + simpl.
    destruct Z.eq_dec.
    split;[apply h1|].
    simpl; unfold is_intR.
    change 0 with (Z2R 0).
    now rewrite Zfloor_Z2R.
    change (is_int (of_int RTZ (to_int m (B754_finite b m0 e e0)))).
    apply of_int_is_int.
    apply is_finite_to_int2.
    assumption.
Qed.

(* Why3 goal *)
Lemma eq_is_int : forall (x:t) (y:t), (eq x y) -> ((is_int x) -> (is_int y)).
Proof.
  intros x y h1 (h2,h3).
  unfold is_int.
  split; [apply (eq_finite_dist h1); auto|].
  unfold is_intR in *.
  apply to_real_eq_alt in h1.
  rewrite h1 in *; assumption.
Qed.

(* Why3 goal *)
Lemma add_int : forall (x:t) (y:t) (m:ieee_float.RoundingMode.mode), (is_int
  x) -> ((is_int y) -> ((is_finite (add m x y)) -> (is_int (add m x y)))).
Proof.
intros x y m (h1,h1') (h2,h2') h3.
destruct (add_finite_rev_n' m x y h3).
+ destruct H.
  unfold is_int.
  split; auto.
  rewrite H0.
  apply is_intR_round.
  apply is_intR_equiv.
  exists (floor (to_real x) + floor (to_real y))%Z.
  unfold is_intR in h1', h2'; rewrite h1', h2' at 1.
  symmetry; apply Z2R_plus.
+ split; auto.
  rewrite max_real_int, <-Z2R_IZR in H.
  destruct H; apply is_intR_equiv.
  exists max_int; assumption.
  exists (- max_int)%Z.
  rewrite Z2R_opp; assumption.
Qed.

(* Why3 goal *)
Lemma sub_int : forall (x:t) (y:t) (m:ieee_float.RoundingMode.mode), (is_int
  x) -> ((is_int y) -> ((is_finite (sub m x y)) -> (is_int (sub m x y)))).
Proof.
intros x y m (h1,h1') (h2,h2') h3.
destruct (sub_finite_rev_n' m x y h3).
+ destruct H.
  unfold is_int.
  split; auto.
  rewrite H0.
  apply is_intR_round.
  apply is_intR_equiv.
  exists (floor (to_real x) - floor (to_real y))%Z.
  unfold is_intR in h1', h2'; rewrite h1', h2' at 1.
  symmetry; apply Z2R_minus.
+ split; auto.
  rewrite max_real_int, <-Z2R_IZR in H.
  destruct H; apply is_intR_equiv.
  exists max_int; assumption.
  exists (- max_int)%Z.
  rewrite Z2R_opp; assumption.
Qed.

(* Why3 goal *)
Lemma mul_int : forall (x:t) (y:t) (m:ieee_float.RoundingMode.mode), (is_int
  x) -> ((is_int y) -> ((is_finite (mul m x y)) -> (is_int (mul m x y)))).
Proof.
intros x y m (h1,h1') (h2,h2') h3.
destruct (mul_finite_rev_n' m x y h3).
+ destruct H.
  unfold is_int.
  split; auto.
  rewrite H0.
  apply is_intR_round.
  apply is_intR_equiv.
  exists (floor (to_real x) * floor (to_real y))%Z.
  unfold is_intR in h1', h2'; rewrite h1', h2' at 1.
  symmetry; apply Z2R_mult.
+ split; auto.
  rewrite max_real_int, <-Z2R_IZR in H.
  destruct H; apply is_intR_equiv.
  exists max_int; assumption.
  exists (- max_int)%Z.
  rewrite Z2R_opp; assumption.
Qed.

(* Why3 goal *)
Lemma fma_int : forall (x:t) (y:t) (z:t) (m:ieee_float.RoundingMode.mode),
  (is_int x) -> ((is_int y) -> ((is_int z) -> ((is_finite (fma m x y z)) ->
  (is_int (fma m x y z))))).
Proof.
intros x y z m (h1,h1') (h2,h2') (h3,h3') h4.
destruct (fma_finite_rev_n' m x y z h4).
+ destruct H.
  unfold is_int.
  split; auto.
  rewrite H0.
  apply is_intR_round.
  apply is_intR_equiv.
  exists (floor (to_real x) * floor (to_real y) + floor (to_real z))%Z.
  unfold is_intR in h1', h2', h3'; rewrite h1', h2', h3' at 1.
  rewrite Z2R_plus, Z2R_mult; reflexivity.
+ split; auto.
  rewrite max_real_int, <-Z2R_IZR in H.
  destruct H; apply is_intR_equiv.
  exists max_int; assumption.
  exists (- max_int)%Z.
  rewrite Z2R_opp; assumption.
Qed.

(* Why3 goal *)
Lemma neg_int : forall (x:t), (is_int x) -> (is_int (neg x)).
Proof.
intros x (h1,h2).
destruct (neg_finite x h1).
split; try easy.
unfold is_intR in *.
rewrite H0.
rewrite h2 at 2.
rewrite <-Z2R_opp, Zfloor_Z2R, Z2R_opp.
apply f_equal, h2.
Qed.

(* Why3 goal *)
Lemma abs_int : forall (x:t), (is_int x) -> (is_int (abs x)).
Proof.
intros x (h1,h2).
destruct (abs_finite x h1) as (h3,(h4,h5)).
split; try easy.
unfold is_intR in *.
rewrite h4.
rewrite h2 at 2.
rewrite <-Z2R_abs, Zfloor_Z2R, Z2R_abs.
apply f_equal, h2.
Qed.

(* Why3 goal *)
Lemma is_int_of_int : forall (x:t) (m:ieee_float.RoundingMode.mode)
  (m':ieee_float.RoundingMode.mode), (is_int x) -> (eq x (of_int m' (to_int m
  x))).
Proof.
  intros x m m' h1.
  assert (h1':=h1).
  destruct h1 as (h1,h2).
  assert (no_overflow m' (IZR (to_int m x))) by
      (apply is_finite_to_int; auto).
  destruct (of_int_correct H) as (h3,(h4,h5)); auto.
  rewrite to_real_eq; auto.
  rewrite h3, <-int_to_real_; auto.
  symmetry; apply Round_to_real; auto.
Qed.

(* Why3 goal *)
Lemma is_int_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int
  x) -> (in_int_range (to_int m x)).
Proof.
intros m x h1.
pose proof (@int_to_real_ m x h1).
unfold in_int_range.
destruct h1.
apply is_finite1 in H0.
unfold in_range in H0.
destruct H0.
split; apply le_IZR; try rewrite FromInt.Neg; rewrite <-max_real_int, <-H; auto.
Qed.

(* Why3 goal *)
Lemma is_int_is_finite : forall (x:t), (is_int x) -> (is_finite x).
Proof.
intros x (h,_); assumption.
Qed.

(* Why3 goal *)
Lemma int_to_real : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int
  x) -> ((to_real x) = (BuiltIn.IZR (to_int m x))).
Proof.
intros m x.
apply int_to_real_.
Qed.

Lemma of_int_to_real : forall (m:mode) (x:Z), (no_overflow m
  (BuiltIn.IZR x)) -> ((to_real (of_int m x)) = (round m
  (BuiltIn.IZR x))).
Proof.
  intros m x h1.
  apply (of_int_correct h1).
Qed.

(* TODO: add to theory ? *)
Lemma to_real_roundToIntegral: forall {x} m, is_finite x -> to_real (roundToIntegral m x) = Z2R (to_int m x).
Proof.
  intros x m h.
  unfold roundToIntegral.
  destruct Z.eq_dec.

  destruct x; try easy.
  rewrite B754_zero_to_real, e; auto.
  rewrite B754_zero_to_real, e; auto.

  destruct x; try easy.
  contradict n.
  apply to_int_B754_zero.

  set (x:= B754_finite b m0 e e0); fold x in h, h.
  change (to_real (of_int RTZ (to_int m x)) = Z2R (to_int m x)).

  assert (is_finite Bmax_rep_int) by auto.
  destruct (neg_finite _ H) as (H0,_).

  assert (((le (neg Bmax_rep_int) x) /\ (le x Bmax_rep_int))
       \/ ((le x (neg Bmax_rep_int)) \/ (le Bmax_rep_int x))) as h1.
  destruct (le_or_lt_or_nan x Bmax_rep_int) as [h1|[h1|[h1|h1]]].
  + destruct (le_or_lt_or_nan (neg Bmax_rep_int) x) as [h2|[h2|[h2|h2]]].
    - left; split; easy.
    - right; left; apply lt_le; auto.
    - destruct (neg Bmax_rep_int); easy.
    - destruct x; easy.
  + right; right; apply lt_le; auto.
  + destruct x; easy.
  + destruct Bmax_rep_int; easy.

  + destruct h1.
    - destruct H1.
      apply (@to_int_le _ _ m H0 h) in H1.
      apply (@to_int_le _ _ m h H) in H2.
      rewrite (neg_int_to_int Bmax_rep_int_is_int) in H1.
      rewrite Bmax_rep_int_to_int in H1, H2.
      rewrite of_int_to_real.
      rewrite Exact_rounding_for_integers; auto.
      rewrite Z2R_IZR; reflexivity.
      unfold in_safe_int_range; auto.
      apply Bounded_real_no_overflow.
      apply rep_int_in_range; auto.
    - rewrite (@Bmax_rep_int_of_int m) in H1.
      pose proof (big_float_is_int m _ h H1).
      rewrite of_int_to_real.
      rewrite <-int_to_real; auto.
      rewrite Round_to_real; auto.
      rewrite Z2R_IZR.
      apply int_to_real; auto.
      apply Bounded_real_no_overflow.
      apply is_finite_range_to_int; auto.
Qed.

(* Why3 goal *)
Lemma truncate_int : forall (m:ieee_float.RoundingMode.mode) (i:t), (is_int
  i) -> (eq (roundToIntegral m i) i).
Proof.
  intros m i (h1,h2).
  pose proof (roundToIntegral_finite m h1).
  rewrite eq_to_real_finite; auto.
  rewrite to_real_roundToIntegral; auto.
  rewrite Z2R_IZR.
  symmetry.
  apply int_to_real; auto.
Qed.

(* Why3 goal *)
Lemma truncate_neg : forall (x:t), (is_finite x) -> ((is_negative x) ->
  ((roundToIntegral ieee_float.RoundingMode.RTZ
  x) = (roundToIntegral ieee_float.RoundingMode.RTP x))).
Proof.
  intros x h1 h2.
  destruct x; try easy.
  simpl roundToIntegral.
  pose proof (negative_to_real _ h1 h2).
  pose proof (Ztrunc_ceil _ H).
  simpl in H0.
  rewrite H0.
  reflexivity.
Qed.

(* Why3 goal *)
Lemma truncate_pos : forall (x:t), (is_finite x) -> ((is_positive x) ->
  ((roundToIntegral ieee_float.RoundingMode.RTZ
  x) = (roundToIntegral ieee_float.RoundingMode.RTN x))).
Proof.
  intros x h1 h2.
  destruct x; try easy.
  simpl roundToIntegral.
  pose proof (positive_to_real _ h1 h2).
  pose proof (Ztrunc_floor _ H).
  simpl in H0.
  rewrite H0.
  reflexivity.
Qed.

(* Why3 goal *)
Lemma ceil_le : forall (x:t), (is_finite x) -> (le x
  (roundToIntegral ieee_float.RoundingMode.RTP x)).
Proof.
intros x h1.
pose proof (roundToIntegral_finite RTP h1).
rewrite le_to_real; auto.
rewrite to_real_roundToIntegral; auto.
simpl.
apply Zceil_ub.
Qed.

(* Why3 goal *)
Lemma ceil_lest : forall (x:t) (y:t), ((le x y) /\ (is_int y)) -> (le
  (roundToIntegral ieee_float.RoundingMode.RTP x) y).
Proof.
intros x y (h1,h2).
destruct (le_special _ _ h1) as [h|[h|h]]; try easy.
- destruct h.
  pose proof (roundToIntegral_finite RTP H).
  rewrite le_to_real; auto.
  rewrite to_real_roundToIntegral; auto.
  simpl.
  rewrite (int_to_real RTP _ h2), <-Z2R_IZR.
  apply Z2R_le, Zceil_glb.
  rewrite Z2R_IZR, <-(int_to_real RTP _ h2).
  apply le_to_real; auto.
- destruct h as (h,_).
  unfold is_minus_infinity in h.
  destruct x; easy.
- unfold is_plus_infinity in h.
  destruct h, h2, y; try easy.
Qed.

(* Why3 goal *)
Lemma ceil_to_real : forall (x:t), (is_finite x) ->
  ((to_real (roundToIntegral ieee_float.RoundingMode.RTP
  x)) = (BuiltIn.IZR (real.Truncate.ceil (to_real x)))).
Proof.
  intros x h.
  rewrite to_real_roundToIntegral; auto.
  unfold to_int.
  rewrite Z2R_IZR; reflexivity.
Qed.

(* Why3 goal *)
Lemma ceil_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_finite
  x) -> ((to_int m (roundToIntegral ieee_float.RoundingMode.RTP
  x)) = (real.Truncate.ceil (to_real x))).
Proof.
  intros m x h.
  unfold to_int.
  rewrite to_real_roundToIntegral; auto.
  destruct (valid_rnd_round_mode m) as (_,h').
  destruct m; apply (h' (to_int RTP x)).
Qed.

(* Why3 goal *)
Lemma floor_le : forall (x:t), (is_finite x) -> (le
  (roundToIntegral ieee_float.RoundingMode.RTN x) x).
Proof.
  intros x h1.
  pose proof (roundToIntegral_finite RTN h1).
  rewrite le_to_real; auto.
  rewrite to_real_roundToIntegral; auto.
  simpl.
  apply Zfloor_lb.
Qed.

(* Why3 goal *)
Lemma floor_lest : forall (x:t) (y:t), ((le y x) /\ (is_int y)) -> (le y
  (roundToIntegral ieee_float.RoundingMode.RTN x)).
Proof.
  intros x y (h1,h2).
  destruct (le_special _ _ h1) as [h|[h|h]]; try easy.
  - destruct h.
    pose proof (roundToIntegral_finite RTN H0).
    rewrite le_to_real; auto.
    rewrite to_real_roundToIntegral; auto.
    simpl.
    rewrite (int_to_real RTN _ h2), <-Z2R_IZR.
    apply Z2R_le, Zfloor_lub.
    rewrite Z2R_IZR, <-(int_to_real RTN _ h2).
    apply le_to_real; auto.
  - destruct h2 as (h2,_).
    unfold is_minus_infinity in h.
    destruct y; easy.
  - unfold is_plus_infinity in h.
    destruct h; destruct H; destruct H0, h2, x; try easy.
Qed.

(* Why3 goal *)
Lemma floor_to_real : forall (x:t), (is_finite x) ->
  ((to_real (roundToIntegral ieee_float.RoundingMode.RTN
  x)) = (BuiltIn.IZR (real.Truncate.floor (to_real x)))).
Proof.
  intros x h.
  rewrite to_real_roundToIntegral; auto.
  unfold to_int.
  rewrite Z2R_IZR; reflexivity.
Qed.

(* Why3 goal *)
Lemma floor_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (is_finite x) -> ((to_int m (roundToIntegral ieee_float.RoundingMode.RTN
  x)) = (real.Truncate.floor (to_real x))).
Proof.
  intros m x h.
  unfold to_int.
  rewrite to_real_roundToIntegral; auto.
  destruct (valid_rnd_round_mode m) as (_,h').
  destruct m; apply (h' (to_int RTN x)).
Qed.

Lemma same_sign_roundToIntegral:
  forall {x} (m:mode), ~ is_nan x -> same_sign (roundToIntegral m x) x.
Proof.
  intros x m h.
  unfold same_sign.
  destruct x; try (now elim h); try (destruct b; simpl; now auto); clear h.
  set (x:=B754_finite b m0 e e0).
  assert (no_overflow RTZ (IZR (to_int m x))) by
      now apply is_finite_to_int.
  destruct (of_int_correct H) as (_,(_,h1)); clear H.
  assert (is_finite x) as h2 by easy.
  pose proof (roundToIntegral_finite m h2).
  destruct b; simpl;[right|left];split;auto.
  + apply is_negative_Bsign; auto.
    change (~ is_nan (roundToIntegral m x)); destruct (roundToIntegral m x); easy.
    assert (to_int m x <= 0)%Z.
    apply is_negative_to_int; easy.
    destruct (Z_le_lt_eq_dec _ _ H0).
    - rewrite Zcompare_Lt in h1 by auto.
      destruct Z.eq_dec; auto.
    - destruct Z.eq_dec; auto.
  + apply is_positive_Bsign; auto.
    change (~ is_nan (roundToIntegral m x)); destruct (roundToIntegral m x); easy.
    assert (0 <= to_int m x)%Z.
    apply is_positive_to_int; easy.
    destruct (Z_le_lt_eq_dec _ _ H0).
    - rewrite Zcompare_Gt in h1 by auto.
      destruct Z.eq_dec; auto.
    - symmetry in e1.
      destruct Z.eq_dec; easy.
Qed.

Lemma same_sign_roundToIntegral2:
  forall {x} {m m':mode}, ~ is_nan x -> same_sign (roundToIntegral m x) (roundToIntegral m' x).
Proof.
  intros x m m' h.
  pose proof (same_sign_roundToIntegral m h).
  pose proof (same_sign_roundToIntegral m' h).
  unfold same_sign in *.
  pose proof (negative_xor_positive x).
  destruct H as [(H,H')|(H,H')], H0 as [(H0,H0')|(H0,H0')]; auto.
  contradict H1; auto.
  contradict H1; auto.
Qed.

Lemma no_overflow_to_real_min_RTN:
  forall x, is_finite x -> no_overflow RNE (to_real x - to_real (roundToIntegral RTN x)).
Proof.
  intros x h.
  rewrite to_real_roundToIntegral; auto.
  unfold to_int.
  apply Bounded_real_no_overflow.
  pose proof (Zfloor_ub (to_real x)).
  pose proof (Zfloor_lb (to_real x)).
  unfold in_range.
  pose proof max_real_ge_6.
  fold (to_real x).
  split; fourier.
Qed.

Lemma ceil_lb: forall x, ((Z2R (ceil x) - 1) < x).
Proof.
  intro.
  case (Req_dec (Z2R (Zfloor x)) x); intro.
  rewrite <-H, Zceil_Z2R, H; simpl; fourier.
  rewrite (Zceil_floor_neq _ H).
  rewrite Z2R_plus; simpl.
  pose proof (Zfloor_lb x).
  destruct (Rle_lt_or_eq_dec _ _ H0); try easy.
  fourier.
Qed.

Lemma no_overflow_to_real_RTP_min:
  forall x, is_finite x -> no_overflow RNE (to_real (roundToIntegral RTP x) - to_real x).
Proof.
  intros x h.
  rewrite to_real_roundToIntegral; auto.
  unfold to_int.
  apply Bounded_real_no_overflow.
  pose proof (Zceil_ub (to_real x)).
  pose proof (ceil_lb (to_real x)).
  unfold in_range.
  pose proof max_real_ge_6.
  fold (to_real x).
  split; fourier.
Qed.

(* Why3 goal *)
Lemma RNA_down : forall (x:t), (lt (sub ieee_float.RoundingMode.RNE x
  (roundToIntegral ieee_float.RoundingMode.RTN x))
  (sub ieee_float.RoundingMode.RNE
  (roundToIntegral ieee_float.RoundingMode.RTP x) x)) ->
  ((roundToIntegral ieee_float.RoundingMode.RNA
  x) = (roundToIntegral ieee_float.RoundingMode.RTN x)).
Proof.
  intros x h.
  destruct x; try easy.
  set (x:=(B754_finite b m e e0)); fold x in h.
  assert (forall m', is_finite (roundToIntegral m' x)) as h1.
  intro m'.
  apply roundToIntegral_finite; try easy.
  apply to_real_refl; try easy.
  2: apply same_sign_roundToIntegral2; easy.

  rewrite to_real_roundToIntegral, to_real_roundToIntegral; try easy.
  f_equal.
  unfold to_int.
  apply Znearest_imp.
  rewrite Rabs_pos_eq.
  2: pose proof (Zfloor_lb (to_real x)); fold (to_real x); fourier.

  assert (is_finite x) as x_fin by easy.
  pose proof (no_overflow_to_real_min_RTN _ x_fin) as h2.
  pose proof (no_overflow_to_real_RTP_min _ x_fin) as h3.

  assert (is_finite (roundToIntegral RTN x)) as rtn_fin by auto.
  assert (is_finite (roundToIntegral RTP x)) as rtp_fin by auto.
  destruct (sub_finite _ _ _ x_fin rtn_fin h2) as (h4,h4').
  destruct (sub_finite _ _ _ rtp_fin x_fin h3) as (h5,h5').
  clear x_fin h2 h3 rtn_fin rtp_fin.

  rewrite lt_finite in h; auto.
  rewrite h4' in h; auto.
  rewrite h5' in h; auto.

  fold (to_real x).
  case (Req_dec (Z2R (Zfloor (to_real x))) (to_real x)); intro.
  fourier.

  apply round_lt in h.
  rewrite to_real_roundToIntegral, to_real_roundToIntegral in h; try easy.
  unfold to_int in h.
  rewrite Zceil_floor_neq, Z2R_plus in h; auto.
  simpl (Z2R 1) in h.
  fold (to_real x) in h.
  fourier.
Qed.

(* Why3 goal *)
Lemma RNA_up : forall (x:t), (lt (sub ieee_float.RoundingMode.RNE
  (roundToIntegral ieee_float.RoundingMode.RTP x) x)
  (sub ieee_float.RoundingMode.RNE x
  (roundToIntegral ieee_float.RoundingMode.RTN x))) ->
  ((roundToIntegral ieee_float.RoundingMode.RNA
  x) = (roundToIntegral ieee_float.RoundingMode.RTP x)).
Proof.
  intros x h.
  destruct x; try easy.
  set (x:=(B754_finite b m e e0)); fold x in h.
  assert (forall m', is_finite (roundToIntegral m' x)) as h1.
  intro m'.
  apply roundToIntegral_finite; try easy.
  apply to_real_refl; try easy.
  2: apply same_sign_roundToIntegral2; easy.

  rewrite to_real_roundToIntegral, to_real_roundToIntegral; try easy.
  f_equal.
  unfold to_int.
  apply Znearest_imp.
  rewrite Rabs_left1.
  2: pose proof (Zceil_ub (to_real x)); fold (to_real x); fourier.
  rewrite Ropp_minus_distr.

  assert (is_finite x) as x_fin by easy.
  pose proof (no_overflow_to_real_min_RTN _ x_fin) as h2.
  pose proof (no_overflow_to_real_RTP_min _ x_fin) as h3.

  assert (is_finite (roundToIntegral RTN x)) as rtn_fin by auto.
  assert (is_finite (roundToIntegral RTP x)) as rtp_fin by auto.
  destruct (sub_finite _ _ _ x_fin rtn_fin h2) as (h4,h4').
  destruct (sub_finite _ _ _ rtp_fin x_fin h3) as (h5,h5').
  clear x_fin h2 h3 rtn_fin rtp_fin.

  rewrite lt_finite in h; auto.
  rewrite h4' in h; auto.
  rewrite h5' in h; auto.

  fold (to_real x).
  case (Req_dec (Z2R (Zceil (to_real x))) (to_real x)); intro.
  fourier.

  apply round_lt in h.
  rewrite to_real_roundToIntegral, to_real_roundToIntegral in h; try easy.
  unfold to_int in h.
  assert (Z2R (floor (to_real x)) <> to_real x).
  intro.
  rewrite <-H0 in H.
  rewrite Zceil_Z2R in H.
  auto.

  rewrite Zceil_floor_neq, Z2R_plus in h; auto.
  rewrite Zceil_floor_neq, Z2R_plus; auto.
  simpl (Z2R 1) in *; fold (to_real x) in h; fourier.
Qed.

Lemma sterbenz_round: forall x y m,
    to_real y / 2 <= to_real x <= 2 * to_real y ->
    round m (to_real x - to_real y) = to_real x - to_real y.
Proof.
  intros x y m h.
  assert (generic_format radix2 fexp (to_real x - to_real y)).
  { Require Flocq.Prop.Fprop_Sterbenz.
    apply Fprop_Sterbenz.sterbenz; auto.
    apply fexp_monotone.
    apply generic_format_B2R.
    apply generic_format_B2R. }
  apply round_generic; auto.
  apply valid_rnd_round_mode.
Qed.

Lemma sterbenz_round_opp: forall x y m,
    to_real y / 2 <= to_real x <= 2 * to_real y ->
    round m (to_real y - to_real x) = to_real y - to_real x.
Proof.
  intros x y m h.
  assert (generic_format radix2 fexp (to_real y - to_real x)).
  { Require Flocq.Prop.Fprop_Sterbenz.
    replace (to_real y - to_real x) with (- (to_real x - to_real y)) by ring.
    apply generic_format_opp.
    apply Fprop_Sterbenz.sterbenz; auto.
    apply fexp_monotone.
    apply generic_format_B2R.
    apply generic_format_B2R. }
  apply round_generic; auto.
  apply valid_rnd_round_mode.
Qed.

Lemma sterbenz_round_2: forall x y m, is_finite y -> is_finite x ->
    2 * to_real y <= to_real x <= to_real y / 2 ->
    round m (to_real x - to_real y) = to_real x - to_real y.
Proof.
  intros x y m h h' h2.
  replace (to_real x - to_real y) with (-to_real y - (- to_real x)) by field.
  destruct (neg_finite _ h) as (_,h1); rewrite <-h1;
  destruct (neg_finite _ h') as (_,h1'); rewrite <-h1'.
  apply sterbenz_round_opp.
  rewrite h1, h1'.
  destruct h2.
  assert (forall x, -x = -1*x) as h2 by (intro; ring).
  split.
  - rewrite h2, (h2 (to_real x)).
    rewrite Real.assoc_mul_div by (apply not_eq_sym, Rlt_not_eq; fourier).
    apply Rmult_le_compat_neg_l; fourier.
  - rewrite h2, (h2 (to_real y)).
    replace (2 * (-1 * to_real y)) with (-1 * (2 * to_real y)) by field.
    apply Rmult_le_compat_neg_l; fourier.
Qed.

Lemma RTN_not_far: forall x,
    is_finite x -> 1 <= to_real x ->
    to_real (roundToIntegral RTN x) / 2 <= to_real x <= 2 * to_real (roundToIntegral RTN x).
Proof.
  intros x h h1.
  rewrite floor_to_real; auto.
  pose proof (Zfloor_lb (to_real x));
  pose proof (Zfloor_ub (to_real x)).
  rewrite <-Z2R_IZR.
  split; try fourier.
  apply Rlt_le.
  apply Rlt_le_trans with (r2:=(Z2R (floor (to_real x)) + 1)); auto.
  assert (1 <= Z2R (floor (to_real x))).
  { pose proof (Rle_lt_trans _ _ _ h1 H0).
    change 1 with (Z2R 1) in *.
    rewrite <-Z2R_plus in H1.
    apply lt_Z2R in H1.
    apply Z2R_le.
    auto with zarith. }
  fourier.
Qed.

Lemma RTN_not_far_opp: forall x,
    is_finite x -> to_real x <= -/2 ->
    2 * to_real (roundToIntegral RTN x) <= to_real x <= to_real (roundToIntegral RTN x) / 2.
Proof.
  intros x h h1.
  rewrite floor_to_real; auto.
  pose proof (Zfloor_lb (to_real x));
  pose proof (Zfloor_ub (to_real x)).
  rewrite <- (Z2R_IZR (floor _)).
  split; try fourier.
  destruct (Rle_lt_dec (to_real x) (-1)); try fourier.
  assert (Z2R(floor (to_real x)) = -1).
  { assert (Z2R(floor(to_real x)) < Z2R 0) by (simpl Z2R; fourier).
    assert (Z2R(-2) < Z2R(floor(to_real x))) by (simpl Z2R; fourier).
    apply lt_Z2R in H1; apply lt_Z2R in H2.
    now replace (floor (to_real x)) with (-1)%Z by omega. }
  fourier.
Qed.

Lemma RTP_not_far: forall x,
    is_finite x -> /2 <= to_real x ->
    to_real x / 2 <= to_real (roundToIntegral RTP x) <= 2 * to_real x.
Proof.
  intros x h h1.
  rewrite ceil_to_real; auto.
  pose proof (ceil_lb (to_real x));
  pose proof (Zceil_ub (to_real x)).
  rewrite <- (Z2R_IZR (ceil _)).
  split; try fourier.
  destruct (Rle_lt_dec 1 (to_real x) ); try fourier.
  assert (Z2R (ceil (to_real x)) = 1).
  { assert (Z2R 0 < Z2R(ceil(to_real x))) by (simpl Z2R; fourier).
    assert (Z2R(ceil(to_real x)) < Z2R(2)) by (simpl Z2R; fourier).
    apply lt_Z2R in H1; apply lt_Z2R in H2.
    now replace (ceil (to_real x)) with 1%Z by omega. }
  fourier.
Qed.

Lemma RTP_not_far_opp: forall x,
    is_finite x -> to_real x <= -1 ->
    2 * to_real x <= to_real (roundToIntegral RTP x) <= to_real x / 2.
Proof.
  intros x h h1.
  rewrite ceil_to_real; auto.
  pose proof (ceil_lb (to_real x));
  pose proof (Zceil_ub (to_real x)).
  rewrite <- (Z2R_IZR (ceil _)).
  split; try fourier.
  apply Rmult_le_reg_r with (r:=2); try fourier.
  replace (to_real x / 2 * 2) with (to_real x) by field.
  apply Rlt_le.
  apply Rle_lt_trans with (r2:=(Z2R (ceil (to_real x)) - 1)); auto.
  assert (Z2R (ceil (to_real x)) <= -1).
  { pose proof (Rlt_le_trans _ _ _ H h1).
    rewrite <- (Z2R_minus _ 1) in H1.
    apply (lt_Z2R _ (-1)) in H1.
    apply (Z2R_le _ (-1)).
    auto with zarith. }
  fourier.
Qed.

Lemma round_plus_weak: forall x y m,
    Rabs (to_real x + to_real y) <= Rmin (Rabs (to_real x)) (Rabs (to_real y)) ->
    round m (to_real x + to_real y) = to_real x + to_real y.
Proof.
  intros x y m h.
  assert (generic_format radix2 fexp (to_real x + to_real y)).
  { Require Flocq.Prop.Fprop_Sterbenz.
    apply Fprop_Sterbenz.generic_format_plus_weak; auto.
    apply fexp_monotone.
    apply generic_format_B2R.
    apply generic_format_B2R. }
  apply round_generic; auto.
  apply valid_rnd_round_mode.
Qed.

Lemma half_bounded: bounded sb emax (shift_pos (sb_pos - 1) 1) (- sb) = true.
Proof.
  unfold bounded.
  apply Bool.andb_true_iff; split.
  unfold canonic_mantissa.
  apply Zeq_bool_true.
  rewrite Fcore_digits.Zpos_digits2_pos, shift_pos_correct.
  rewrite Zmult_1_r, Z.pow_pos_fold.
  rewrite Fcore_digits.Zdigits_Zpower by easy.
  rewrite Pos2Z.inj_sub by exact sb_gt_1.
  fold sb.
  unfold FLT_exp.
  replace (sb - 1 + 1 + - sb)%Z with 0%Z by ring.
  apply Zmax_l.
  pose sb_gt_1; pose Hemax'; omega.
  apply Zle_bool_true.
  pose Hemax'; pose sb_gt_1; omega.
Qed.

Definition half: t.
Proof.
  exact (B754_finite false _ _ half_bounded).
Defined.

Lemma half_to_real : ((to_real half) = (05 / 10)%R).
Proof.
  unfold B2R, half; simpl.
  rewrite shift_pos_correct.
  rewrite Z.pow_pos_fold.
  unfold F2R.
  unfold Fnum, Fexp.
  rewrite Zmult_1_r.
  change 2%Z with (radix_val radix2).
  rewrite Z2R_Zpower by easy.
  rewrite <-bpow_plus.
  rewrite Pos2Z.inj_sub by exact sb_gt_1.
  rewrite <-Pos2Z.opp_pos.
  replace (Z.pos sb_pos - 1 + - Z.pos sb_pos)%Z with (- 1)%Z by ring.
  unfold bpow.
  replace (Z.pow_pos radix2 1)%Z with 2%Z by auto with zarith.
  unfold Z2R, P2R.
  field.
Qed.

Lemma eq_diff_floor_ceil: forall {x}, eq (sub RNE x (roundToIntegral RTN x)) (sub RNE (roundToIntegral RTP x) x) -> to_real x - Z2R (floor (to_real x)) = Z2R (ceil (to_real x)) - to_real x.
Proof.
  intros x h.
  destruct x; try easy.
  - rewrite B754_zero_to_real.
    replace 0 with (Z2R 0) by auto.
    rewrite Zfloor_Z2R, Zceil_Z2R; auto.
  - simpl.
    replace 0 with (Z2R 0) by auto.
    rewrite Zfloor_Z2R, Zceil_Z2R; auto.
  - set (x:=(B754_finite b m e e0)); fold x in h.
    assert (forall m', is_finite (roundToIntegral m' x)) as h1 by
          (intro m'; apply roundToIntegral_finite; easy).

    assert (is_finite x) as x_fin by easy.
    pose proof (no_overflow_to_real_min_RTN _ x_fin) as h2.
    pose proof (no_overflow_to_real_RTP_min _ x_fin) as h3.

    assert (is_finite (roundToIntegral RTN x)) as rtn_fin by auto.
    assert (is_finite (roundToIntegral RTP x)) as rtp_fin by auto.
    destruct (sub_finite _ _ _ x_fin rtn_fin h2) as (h4,h4').
    destruct (sub_finite _ _ _ rtp_fin x_fin h3) as (h5,h5').
    clear h2 h3 rtn_fin rtp_fin.

    assert (h':=h).
    rewrite to_real_eq in h; auto.
    rewrite h4' in h; auto.
    rewrite h5' in h; auto.
    clear h4' h5'.

    destruct (Rle_lt_dec 1 (to_real x));[|destruct (Rle_lt_dec (to_real x) (-1))].

    + destruct (RTN_not_far x); auto.
      destruct (RTP_not_far x); auto; try fourier.
      rewrite sterbenz_round, sterbenz_round in h by auto.
      rewrite to_real_roundToIntegral, to_real_roundToIntegral in h; auto.

    + destruct (RTN_not_far_opp x); auto; try fourier.
      destruct (RTP_not_far_opp x); auto.
      rewrite sterbenz_round_2, sterbenz_round_2 in h by auto.
      rewrite to_real_roundToIntegral, to_real_roundToIntegral in h; auto.

    + destruct (Rle_lt_dec (to_real x) 0).
      destruct r1.
      * assert (floor (to_real x) = (-1)%Z) by
            (apply Zfloor_imp; simpl Z2R; split; fourier).
        assert (ceil (to_real x) = 0%Z) by
            (apply Zceil_imp; simpl Z2R; split; fourier).

        revert h.
        rewrite (to_real_roundToIntegral RTP) by easy.
        unfold to_int.
        fold (to_real x).
        rewrite H1.
        replace (Z2R 0 - to_real x) with (- to_real x) by (simpl Z2R; ring).
        rewrite <-(proj2 (neg_finite _ x_fin)).
        rewrite (Round_to_real RNE) by easy.
        rewrite (proj2 (neg_finite _ x_fin)).

        { destruct (Rle_lt_dec (to_real x) (-/2)).
        - assert (
               round RNE (to_real x - to_real (roundToIntegral RTN x)) =
               to_real x - to_real (roundToIntegral RTN x)) as aux1.
           { rewrite Real.infix_mn_def, <-(proj2 (neg_finite _ (h1 RTN))).
             apply round_plus_weak.
             rewrite (proj2 (neg_finite _ (h1 RTN))).
             rewrite to_real_roundToIntegral; auto.
             unfold to_int.
             fold (to_real x).
             rewrite H0.
             simpl Z2R.
             rewrite Ropp_involutive.
             rewrite Rabs_right, Rabs_left, Rabs_right, Rmin_left; fourier. }
           rewrite aux1.
           now rewrite to_real_roundToIntegral.

        - clear r r0.
           rewrite to_real_roundToIntegral by easy.
           unfold to_int.
           fold (to_real x).
           rewrite H0.
           simpl Z2R.
           replace (to_real x - -(1)) with (to_real x+1) by ring.
           pose proof (Rplus_lt_compat_r 1 _ _ r1).
           apply Rlt_le in H2.
           replace (-/2+1) with (5/10) in H2 by field.
           rewrite <-half_to_real in H2.
           apply (Round_monotonic RNE) in H2.
           rewrite Round_to_real in H2 by easy.
           rewrite half_to_real in H2.
           intros.
           fourier. }
      * assert (floor (to_real x) = 0%Z) by
            (apply Zfloor_imp; simpl Z2R; split; fourier).
        assert (ceil (to_real x) = 0%Z) by
            (apply Zceil_imp; simpl Z2R; split; fourier).
        rewrite H0, H1, H; auto.

      * assert (floor (to_real x) = 0%Z) by
            (apply Zfloor_imp; simpl Z2R; split; fourier).
        assert (ceil (to_real x) = 1%Z) by
            (apply Zceil_imp; simpl Z2R; split; fourier).

        revert h.
        rewrite (to_real_roundToIntegral RTN) by easy.
        unfold to_int.
        fold (to_real x).
        rewrite H.
        replace (to_real x - Z2R 0) with (to_real x) by (simpl Z2R ; ring).
        rewrite (Round_to_real RNE) by easy.

        { destruct (Rle_lt_dec (/2) (to_real x)).
        - assert (
               round RNE (to_real (roundToIntegral RTP x) - to_real x) =
               to_real (roundToIntegral RTP x) - to_real x) as aux1.
           { rewrite Real.infix_mn_def, <-(proj2 (neg_finite _ x_fin)).
             apply round_plus_weak.
             rewrite (proj2 (neg_finite _ x_fin)).
             rewrite to_real_roundToIntegral by easy.
             unfold to_int.
             fold (to_real x).
             rewrite H0.
             simpl Z2R.
             rewrite Rabs_right, Rabs_right, Rabs_left, Rmin_right; fourier. }
           rewrite aux1.
           now rewrite to_real_roundToIntegral.

        - clear r r0.
           rewrite to_real_roundToIntegral by easy.
           unfold to_int.
           fold (to_real x).
           rewrite H0.
           pose proof (Ropp_lt_contravar _ _ r2).
           pose proof (Rplus_lt_compat_l 1 _ _ H1).
           apply Rlt_le in H2.
           replace (1+-/2) with (5/10) in H2 by field.
           rewrite <-half_to_real in H2.
           rewrite <-Real.infix_mn_def in H2.
           apply (Round_monotonic RNE) in H2.
           rewrite Round_to_real in H2 by easy.
           rewrite half_to_real in H2.
           simpl Z2R.
           intros.
           fourier. }
Qed.

(* Why3 goal *)
Lemma RNA_down_tie : forall (x:t), (eq (sub ieee_float.RoundingMode.RNE x
  (roundToIntegral ieee_float.RoundingMode.RTN x))
  (sub ieee_float.RoundingMode.RNE
  (roundToIntegral ieee_float.RoundingMode.RTP x) x)) -> ((is_negative x) ->
  ((roundToIntegral ieee_float.RoundingMode.RNA
  x) = (roundToIntegral ieee_float.RoundingMode.RTN x))).
Proof.
  intros x h h'.
  destruct x; try easy.
  set (x:=(B754_finite b m e e0)); fold x in h, h'.
  assert (forall m', is_finite (roundToIntegral m' x)) as h1 by
        (intro m'; apply roundToIntegral_finite; easy).
  apply to_real_refl; auto.
  2: apply same_sign_roundToIntegral2; easy.
  apply eq_diff_floor_ceil in h.

  rewrite to_real_roundToIntegral, to_real_roundToIntegral; try easy.
  f_equal.
  unfold to_int.
  fold (to_real x).

  destruct (is_int_or_not x).
  rewrite (int_to_real RTZ _ H).
  destruct (valid_rnd_round_mode RNA) as (_,H').
  simpl in H'.
  rewrite <-Z2R_IZR, H', Zfloor_Z2R; reflexivity.

  unfold Znearest.
  rewrite Rcompare_Eq.
  rewrite Zle_bool_false; auto.
  apply lt_Z2R.
  apply Rle_lt_trans with (r2:=to_real x).
  apply Zfloor_lb.
  simpl Z2R; rewrite <-zeroF_to_real.
  apply lt_finite; try easy.
  rewrite is_negative_correct in h'.
  destruct h'; easy.

  rewrite Zceil_floor_neq in h.
  rewrite Z2R_plus in h.
  simpl Z2R at 3 in h.
  apply (Rplus_eq_compat_l (to_real x)) in h.
  apply (Rplus_eq_compat_l (- Z2R (floor (to_real x)))) in h.
  ring_simplify in h.
  replace (-2 * Z2R (floor (to_real x))) with
  (2 * - Z2R (floor (to_real x))) in h by ring.
  rewrite <-Rmult_plus_distr_l in h.
  apply (Rmult_eq_compat_l (/2)) in h.
  field_simplify in h.
  replace (- Z2R (floor (to_real x)) + to_real x) with
  (to_real x - Z2R (floor (to_real x))) in h by ring.
  field_simplify; auto.

  unfold is_int in H.
  apply Decidable.not_and in H.
  destruct H.
  now elim H.
  now apply not_eq_sym.
  now left.
Qed.

(* Why3 goal *)
Lemma RNA_up_tie : forall (x:t), (eq (sub ieee_float.RoundingMode.RNE
  (roundToIntegral ieee_float.RoundingMode.RTP x) x)
  (sub ieee_float.RoundingMode.RNE x
  (roundToIntegral ieee_float.RoundingMode.RTN x))) -> ((is_positive x) ->
  ((roundToIntegral ieee_float.RoundingMode.RNA
  x) = (roundToIntegral ieee_float.RoundingMode.RTP x))).
Proof.
  intros x h h'.
  destruct x; try easy.
  set (x:=(B754_finite b m e e0)); fold x in h, h'.
  assert (forall m', is_finite (roundToIntegral m' x)) as h1 by
        (intro m'; apply roundToIntegral_finite; easy).
  apply to_real_refl; auto.
  2: apply same_sign_roundToIntegral2; easy.
  apply eq_sym, eq_diff_floor_ceil in h.

  rewrite to_real_roundToIntegral, to_real_roundToIntegral; try easy.
  f_equal.
  unfold to_int.
  fold (to_real x).

  destruct (is_int_or_not x).
  rewrite (int_to_real RTZ _ H).
  destruct (valid_rnd_round_mode RNA) as (_,H').
  simpl in H'.
  rewrite <-Z2R_IZR, H', Zceil_Z2R; reflexivity.

  unfold Znearest.
  rewrite Rcompare_Eq.
  rewrite Zle_bool_true; auto.
  apply non_zero_positive_to_real in h'; try easy.
  apply Zfloor_lub.
  simpl Z2R; fourier.
  unfold is_zero.
  unfold eq. simpl.
  destruct b; easy.

  rewrite Zceil_floor_neq in h.
  rewrite Z2R_plus in h.
  simpl Z2R at 3 in h.
  apply (Rplus_eq_compat_l (to_real x)) in h.
  apply (Rplus_eq_compat_l (- Z2R (floor (to_real x)))) in h.
  ring_simplify in h.
  replace (-2 * Z2R (floor (to_real x))) with
  (2 * - Z2R (floor (to_real x))) in h by ring.
  rewrite <-Rmult_plus_distr_l in h.
  apply (Rmult_eq_compat_l (/2)) in h.
  field_simplify in h.
  replace (- Z2R (floor (to_real x)) + to_real x) with
  (to_real x - Z2R (floor (to_real x))) in h by ring.
  field_simplify; auto.

  unfold is_int in H.
  apply Decidable.not_and in H.
  destruct H.
  now elim H.
  now apply not_eq_sym.
  now left.
Qed.

(* Why3 goal *)
Lemma to_int_roundToIntegral : forall (m:ieee_float.RoundingMode.mode) (x:t),
  ((to_int m x) = (to_int m (roundToIntegral m x))).
Proof.
  intros m x.
  destruct x; try easy.
  unfold to_int at 2.
  rewrite to_real_roundToIntegral by easy.
  destruct (valid_rnd_round_mode m) as (_,h).
  pose proof (h (to_int m (B754_finite b m0 e e0))).
  now destruct m.
Qed.

(* Why3 goal *)
Lemma to_int_monotonic : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite x) -> ((is_finite y) -> ((le x y) -> ((to_int m x) <= (to_int m
  y))%Z)).
Proof.
intros m x y h1 h2 h3.
now apply to_int_le.
Qed.

(* Why3 goal *)
Lemma to_int_of_int : forall (m:ieee_float.RoundingMode.mode) (i:Z),
  (in_safe_int_range i) -> ((to_int m (of_int m i)) = i).
Proof.
intros m i (h1,h2).
apply eq_IZR.
rewrite <-int_to_real.
rewrite of_int_to_real.
apply Exact_rounding_for_integers; auto.
unfold in_safe_int_range; auto.
apply Bounded_real_no_overflow, rep_int_in_range; auto.
apply of_int_is_int.
pose proof pow2sb_lt_max_int.
unfold in_int_range; auto with zarith.
Qed.

(* Why3 goal *)
Lemma eq_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (is_finite x) -> ((eq x y) -> ((to_int m x) = (to_int m y))).
Proof.
intros m x y h1 h2.
apply to_int_eq, h2.
Qed.

(* Why3 goal *)
Lemma neg_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int
  x) -> ((to_int m (neg x)) = (-(to_int m x))%Z).
Proof.
intros m x h1.
apply neg_int_to_int; auto.
Qed.

(* Why3 goal *)
Lemma roundToIntegral_is_finite : forall (m:ieee_float.RoundingMode.mode)
  (x:t), (is_finite x) -> (is_finite (roundToIntegral m x)).
Proof.
intros m x h1.
apply roundToIntegral_finite, h1.
Qed.

End GenericFloat.