why3/lib/coq/ieee_float/GenericFloat.v

(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2025 --  Inria - CNRS - Paris-Saclay 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 Psatz.
Require Import ZArith Reals.
Require Import Flocq.Core.Core.
Require Import Flocq.IEEE754.BinarySingleNaN.
Require Import Flocq.Calc.Bracket.
Require Import Flocq.Calc.Round.
Require Import Flocq.Prop.Plus_error.
Require Flocq.Prop.Sterbenz.
Import real.Truncate.
Import ieee_float.RoundingMode.

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

Local Open Scope R_scope.

Definition mode_to_IEEE : mode -> BinarySingleNaN.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 >-> BinarySingleNaN.mode.

Section GenericFloat.

Variable eb_pos sb_pos : positive.

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

(* Why3 goal *)
Definition sb : Numbers.BinNums.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 := cexp 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 (r_to_fp rnd x) = true /\
  B2R (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)) (cexp 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 (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 : SpecFloat.bounded sb emax (2 ^ sb_pos - 1) (emax - sb) = true.
Proof.
  assert (0 <= sb - 1)%Z.
  apply Zlt_0_le_0_pred, Hsb'.
  unfold SpecFloat.bounded; apply Bool.andb_true_iff; split.
  unfold SpecFloat.canonical_mantissa, SpecFloat.fexp, FLT_exp, SpecFloat.emin.
  apply Zeq_bool_true.
  rewrite Digits.Zpos_digits2_pos.
  rewrite (Digits.Zdigits_unique radix2 _ sb).
  assert (sb + (emax - sb) - sb = emax - sb)%Z by ring; 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.
  lia.
  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.

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

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

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

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

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

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

(* Why3 goal *)
Definition fma : ieee_float.RoundingMode.mode -> t -> t -> t -> t.
Proof.
  exact (@Bfma sb emax Hsb' Hemax').
Defined.

(* Why3 goal *)
Definition sqrt : ieee_float.RoundingMode.mode -> t -> t.
Proof.
  exact (@Bsqrt sb emax Hsb' Hemax').
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
         | RNE => ZnearestE
         | RTP => Zceil
         | RTN => Zfloor
         | RTZ => Ztrunc
         end (B2R x)).
Defined.

(* Why3 goal *)
Definition roundToIntegral : ieee_float.RoundingMode.mode -> t -> t.
Proof.
  exact (fun m x =>
           match x with
             | B754_zero b => x
             | B754_infinity b => x
             | B754_nan => x
             | 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 => B754_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 => B754_nan
         end).
Defined.

(* Why3 goal *)
Definition le : t -> t -> Prop.
Proof.
  exact (fun a b => match Bcompare a b with Some Lt | Some Eq => True | _ => False end).
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; unfold lt, le, eq.
  destruct Bcompare as [[ | | ] | ] ; split ; try easy.
  now right.
  now left.
  now intros [|].
  now intros [|].
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; simpl; try destruct s; 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].
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.
  - now right.
  - left. now destruct s.
  - now left.
  - left. now destruct s.
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 s; easy.
Qed.

(* Why3 goal *)
Definition is_nan : t -> Prop.
Proof.
  exact is_nan.
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.
  + now destruct s.
  + now elim H.
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 s; auto.
  destruct H; easy.
  unfold eq.
  rewrite Bcompare_correct by easy.
  now rewrite Rcompare_Eq.
Qed.

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

Lemma lt_not_nan: forall {x y}, lt x y -> ~ is_nan x /\ ~ is_nan y.
Proof.
  intros; destruct x, y; 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, le, lt.
  intros x y.
  rewrite Bcompare_swap.
  case_eq (Bcompare y x).
  intros [| |] ; try now left.
  now (right ; left).
  destruct x, y; auto; easy.
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 x = false).
Proof.
  split.
  destruct x; try destruct s; try easy.
  destruct x; try destruct s; 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; try destruct s; auto; easy.
  intro h; destruct h; destruct x; try destruct s; 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 x = true).
Proof.
  split.
  destruct x; try destruct s; easy.
  destruct x; try destruct s; easy.
Qed.

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

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

Lemma not_nan: forall x, ~ (is_nan x) -> {is_finite x} + {is_infinite x}.
Proof.
  unfold is_nan, is_finite.
  intro x; try 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 s0; easy.
Qed.

Lemma bounded_floats :
  forall x:t, (is_finite x) ->
              Bcompare (abs x) max_value = Some Lt
           \/ Bcompare (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.
  unfold Bcompare.
  simpl; rewrite (Zcompare_Lt _ _ l); auto.
  unfold Bcompare.
  simpl; rewrite (Zcompare_Eq _ _ e1).
  unfold SpecFloat.fexp, FLT_exp, SpecFloat.emin in H1.
  rewrite Digits.Zpos_digits2_pos in H1.
  assert (3 - emax - sb <= 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 (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 (Digits.Zdigits radix2 (Z.pos m) = sb) by auto with zarith; clear H1.
  pose (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 lia.
  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.
  intros x Fx.
  unfold le.
  now destruct (bounded_floats x Fx) as [-> | ->].
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 s; auto.
  exists s; right.
  exists s, 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 plus_infinity : t.
Proof.
exact (B754_infinity false).
Defined.

(* Why3 goal *)
Lemma plus_infinity_spec : is_plus_infinity plus_infinity.
Proof.
unfold is_plus_infinity, plus_infinity.
now simpl.
Qed.

(* Why3 goal *)
Definition minus_infinity : t.
Proof.
exact (B754_infinity true).
Defined.

(* Why3 goal *)
Lemma minus_infinity_spec : is_minus_infinity minus_infinity.
Proof.
unfold is_minus_infinity, minus_infinity.
now simpl.
Qed.

(* Why3 goal *)
Definition not_a_number : t.
Proof.
exact B754_nan.
Defined.

(* Why3 goal *)
Lemma not_a_number_spec : is_nan not_a_number.
Proof.
unfold is_nan, not_a_number.
now simpl.
Qed.

(* Why3 goal *)
Definition to_real : t -> Reals.Rdefinitions.R.
Proof.
  exact B2R.
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; try destruct s; try destruct s0; unfold eq, Bcompare; simpl; 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)%R).
Proof.
intros x y h1 h2.
unfold le.
rewrite (Bcompare_correct _ _ x y h1 h2).
split; intro H.
- apply Rnot_lt_le.
  intros H'.
  now rewrite Rcompare_Gt in H.
- case Rcompare_spec; try easy.
  now apply Rle_not_lt.
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%R.
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; try destruct s; try destruct s0; unfold eq, Bcompare; simpl; 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 -> Reals.Rdefinitions.R ->
  Reals.Rdefinitions.R.
Proof.
  exact (fun m => round radix2 fexp (round_mode m)).
Defined.

(* Why3 goal *)
Definition max_real : Reals.Rdefinitions.R.
Proof.
  exact ((1 - bpow radix2 (- sb)) * bpow radix2 emax)%R.
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, minus_IZR.
  fold sb.
  change 2%Z with (radix_val radix2).
  rewrite IZR_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.
  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 |} = Ropp max_real.
Proof.
  rewrite <-max_real_is_F2R.
  rewrite <- Operations.F2R_opp.
  unfold Operations.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))%R.
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)%R.
Proof.
  rewrite max_real_alt.
  generalize (bpow_gt_0 radix2 (emax - sb)).
  lra.
Qed.

Lemma max_real_ge_6 : (6 <= max_real)%R.
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 (8 <= bpow radix2 emax)%R.
    apply (bpow_le radix2 3).
    lia.
  unfold Zminus.
  rewrite bpow_plus.
  assert (bpow radix2 emax * bpow radix2 (-sb) <= bpow radix2 emax * / 4)%R.
    apply Rmult_le_compat_l.
    apply bpow_ge_0.
    apply (bpow_le radix2 _ (-2)).
    now apply Z.opp_le_mono.
  lra.
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 : Numbers.BinNums.Z.
Proof.
  exact (2 ^ emax - 2 ^ (emax - sb))%Z.
Defined.

(* Why3 goal *)
Lemma max_int_spec :
  (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 minus_IZR.
  change 2%Z with (radix_val radix2).
  rewrite IZR_Zpower, IZR_Zpower by (pose Hsb'; pose Hemax'; auto with zarith).
  apply max_real_alt.
Qed.

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

(* Why3 assumption *)
Definition in_int_range (i:Numbers.BinNums.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)%R.
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:Reals.Rdefinitions.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.
  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 (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).
  simpl.
  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_IZR.
    exact H1.

  - 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:Reals.Rdefinitions.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:Reals.Rdefinitions.R)
    (y:Reals.Rdefinitions.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:Reals.Rdefinitions.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:Reals.Rdefinitions.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:Reals.Rdefinitions.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:Reals.Rdefinitions.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:Reals.Rdefinitions.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 : Numbers.BinNums.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:Numbers.BinNums.Z) : Prop :=
  ((-pow2sb)%Z <= i)%Z /\ (i <= pow2sb)%Z.

Lemma max_rep_int_bounded: SpecFloat.bounded sb emax (shift_pos (sb_pos - 1) 1) 1 = true.
Proof.
  unfold SpecFloat.bounded.
  apply Bool.andb_true_iff; split.
  unfold SpecFloat.canonical_mantissa.
  apply Zeq_bool_true.
  rewrite Digits.Zpos_digits2_pos, shift_pos_correct.
  rewrite Zmult_1_r, Z.pow_pos_fold.
  rewrite Digits.Zdigits_Zpower by easy.
  rewrite Pos2Z.inj_sub by exact sb_gt_1.
  fold sb.
  unfold SpecFloat.fexp, FLT_exp, SpecFloat.emin.
  replace (sb - 1 + 1 + 1 - sb)%Z with 1%Z by ring.
  apply Z.max_l.
  pose sb_gt_1; pose Hemax'; lia.
  apply Zle_bool_true.
  pose Hemax'; pose Hsbb; lia.
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.
  easy.
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 IZR_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:Numbers.BinNums.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 (Z.abs 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.
now rewrite Rmult_1_r.
easy.
simpl; unfold emin; generalize Hsb' Hemax'; lia.
unfold pow2sb in Bz.
change 2%Z with (radix_val radix2) in Bz.
apply generic_format_abs_inv.
rewrite <- abs_IZR, Bz, IZR_Zpower.
apply generic_format_bpow.
unfold FLT_exp, emin.
clear Bz; generalize Hsb' Hemax'.
lia.
apply Zlt_le_weak.
apply Hsb'.
Qed.

(* Why3 goal *)
Definition from_real :
  ieee_float.RoundingMode.mode -> Reals.Rdefinitions.R -> t.
Proof.
  exact r_to_fp. 
Defined.

(* Why3 goal *)
Lemma from_real_in_range :
  forall (m:ieee_float.RoundingMode.mode) (r:Reals.Rdefinitions.R),
  in_range (round m r) ->
  let f := from_real m r in is_finite f /\ ((to_real f) = (round m r)).
Proof.
intros m r h1 f.
unfold from_real, round in *.
unfold is_finite, in_range, to_real in *.
apply r_to_fp_correct.
unfold max_real in *.
Admitted.

(* Why3 goal *)
Lemma from_real_large_neg :
  forall (m:ieee_float.RoundingMode.mode) (r:Reals.Rdefinitions.R),
  ((round m r) < (-max_real)%R)%R ->
  let f := from_real m r in is_infinite f /\ is_negative f.
Proof.
intros m r h1 f.
Admitted.

(* Why3 goal *)
Lemma from_real_large_pos :
  forall (m:ieee_float.RoundingMode.mode) (r:Reals.Rdefinitions.R),
  (max_real < (round m r))%R ->
  let f := from_real m r in is_infinite f /\ is_positive f.
Proof.
intros m r h1 f.
Admitted.

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.
  pose proof pow2sb_lt_max_int.
  split; apply IZR_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 s; 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 s, s0; try easy.
destruct s, s0; try easy.

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

destruct (Z_dec e e1) as [He|He].

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

- destruct He.
  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, Bcompare in h4; simpl in h4.
    destruct s0.
    * 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 s, s0, h4; easy.
  + symmetry in h3.
    apply eq_0_F2R in h3.
    destruct s0; contradict h3; easy.
  + apply eq_0_F2R in h3.
    destruct s; 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; try destruct s; try destruct s0; try destruct s1; 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; try destruct s; try destruct s0; 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).
now apply le_to_real.
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 s, s0, s1; easy).
  set (x:=B754_finite s m e e0);
    set (y:=B754_finite s0 m0 e1 e2);
    set (z:=B754_finite s1 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 (B754_finite s0 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 s, s0, s1; easy).
  set (x:=B754_finite s m e e0);
    set (y:=B754_finite s0 m0 e1 e2);
    set (z:=B754_finite s1 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 (B754_finite s0 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 s, s0, s1; easy).
  set (x:=B754_finite s m e e0);
    set (y:=B754_finite s0 m0 e1 e2);
    set (z:=B754_finite s1 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 (B754_finite s0 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).
  apply le_correct in h.
  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).
  apply le_correct in 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 easy; try (destruct s,s0,h,h1; easy).
set (x:=B754_finite s m e e0);
  set (y:=B754_finite s0 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.
  now destruct Rcompare.
+ apply Rcompare_not_Gt_inv.
  now destruct (Rcompare (B2R y) (B2R x)).
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)); try (try destruct s; try destruct s0; try easy; elim h1; auto; easy).
  revert h.
  unfold le, lt.
  rewrite Bcompare_swap.
  rewrite Bcompare_correct by easy.
  now destruct Rcompare as [| |].
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 (try destruct s; try destruct s0; try easy; elim h1; auto; easy).
  revert h.
  unfold le, lt.
  rewrite Bcompare_swap.
  rewrite Bcompare_correct by easy.
  now destruct Rcompare as [| |].
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 s, s0; auto; destruct h; auto; easy).
  - right; right. destruct s0, h; split; easy.
  - right; left. destruct s, h; split; easy.
  - right. destruct s, s0, h; try easy.
    + left; split; easy.
    + left; split; easy.
    + right; split; easy.
  - right; left. destruct s, h; split; easy.
  - right; right. destruct s, s0, 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 s, s0; easy).

  - right; right. destruct s0; split; try split; easy.
  - right; left. destruct s; split; try split; easy.
  - right; right. destruct s, s0; split; try split; easy.
  - right; left. destruct s; split; try split; easy.
  - right; right. destruct s, s0; 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; try easy; destruct s, s0, s1; 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).
  apply le_correct.
  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 s; 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).
  apply le_correct.
  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 s; 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; try destruct s; 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; try destruct s; 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)); lra.
- destruct r.
  + split; [apply to_real_negative; try easy|apply to_real_positive; easy].
    apply Rmult_lt_reg_r with (r := (to_real y)); lra.
  + rewrite H in h3; lra.
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; lra.
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' 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 s, s0; try easy;
  simpl in h1; unfold is_finite in h1; now rewrite is_finite_build_nan in h1.
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 s0); split; lra.
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 s m0 e e0).
set (y := B754_finite s0 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' m x y H H0).
change (Bplus 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' 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 s, s0; try easy;
    simpl in h1; unfold is_finite in h1; now rewrite is_finite_build_nan in h1.
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 s0); split; lra.
apply Bounded_real_no_overflow.
unfold to_real.
rewrite Rminus_0_l, <- B2R_Bopp.
apply is_finite1, is_finite_Bopp.
apply Bounded_real_no_overflow; rewrite Rminus_0_r; apply is_finite1; auto.
set (x := B754_finite s m0 e e0).
set (y := B754_finite s0 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' m x y H H0).
change (Bminus 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' 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 s, s0; try easy;
    simpl in h1; unfold is_finite in h1; now rewrite is_finite_build_nan in h1.
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 s0); split; lra.
unfold no_overflow; rewrite Rmult_0_l, <-zeroF_to_real, Round_to_real, zeroF_to_real; auto; split; lra.
unfold no_overflow; rewrite Rmult_0_r, <-zeroF_to_real, Round_to_real, zeroF_to_real; auto; split; lra.
set (x := B754_finite s m0 e e0).
set (y := B754_finite s0 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' m x y).
change (Bmult 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' 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;
    simpl in h1; unfold is_finite in h1; try now rewrite is_finite_build_nan in h1.
  right; destruct s, s0; easy.
  left; destruct s, s0; split; try split; easy.
  right; destruct s, s0; split; try split; easy.
  left; destruct s, s0; 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; lra.
    set (x := B754_finite s m0 e e0).
    set (y := B754_finite s0 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' m x y H0).
    change (Bdiv 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 now destruct x.
  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 x).
  apply is_positive_Bsign.
  apply (is_finite_not_nan H).
  apply H1.
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 s, s0; 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')); try destruct s; try easy.
        assert (~ is_nan x) by (rewrite <-is_not_nan1; assumption).
        apply le_infinity.
        destruct x; easy.
    * destruct x, y; try easy.
      destruct s; try easy.
      now destruct s0.
    * now destruct x.

  + intros (_,a).
    destruct y; try easy.
    now destruct x.
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 now destruct x.
split; [easy| apply abs_finite; auto].
Qed.

(* Why3 goal *)
Lemma abs_universal : forall (x:t), ~ is_negative (abs x).
Proof.
intros x.
now destruct x.
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' m x) as (g,(g1,g2)).
  split; auto.
  destruct x; try destruct s; 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).
    destruct x; try destruct s ; try easy;
    simpl in h1; unfold is_finite in h1;
    now rewrite is_finite_build_nan in h1.
  split; [easy|].
  assert (0 <= to_real x).
  { destruct x ; try destruct s; try easy; try apply Rle_refl.
    now apply F2R_ge_0. }
  split; [easy| apply sqrt_finite; auto].
Qed.

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

Lemma sign_FF_overflow : forall m b,
    sign_SF (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:t, sign_SF (B2SF x) = Bsign x.
Proof.
  now destruct x.
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; try easy; destruct s, s0, h; easy.
  - destruct x, y; try easy; destruct s0; auto; easy.
  - destruct x, y; try easy; destruct s; auto; easy.
  - destruct x, y; try easy; destruct s, s0; destruct h2 as [(h2,h3)|(h2,h3)]; auto; easy.
  - destruct x, y; try easy; destruct s, s0; 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' m x y h h1).
    rewrite Rlt_bool_false in H by auto.
    destruct H.
    split.

    + destruct x, y; try easy.
      * destruct s, s0, 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 s0;[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 s;[right;split;[easy|]|left;split;[easy|]]; apply lt_finite; easy.
      * change (Bplus m (B754_finite s m0 e e0) (B754_finite s0 m1 e1 e2)) with r in H.
        pose proof (sign_FF_overflow m (Bsign (B754_finite s 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 s;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).
          lra.
        - 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).
          lra. }

    + change (Bplus m x y) with r in H.
      assert (H':=H).
      apply (f_equal sign_SF) 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 x = true \/ Bsign x = false) by
            (destruct x ; try destruct s; 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, <- SF2R_B2SF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
          now apply Pos.pow_gt_1.
        - 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 x = true \/ Bsign x = false) by
            (destruct x ; try destruct s; 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, <- SF2R_B2SF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            now apply Pos.pow_gt_1.
          + assert (~is_nan r) by
                (destruct r; try easy; destruct n; easy).
            rewrite is_positive_Bsign; easy. }
      * assert (Bsign x = true \/ Bsign x = false) by
            (destruct x ; try destruct s; 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, <- SF2R_B2SF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            now apply Pos.pow_gt_1.
        - 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, <- SF2R_B2SF, H; auto.
            *  rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
               now apply Pos.pow_gt_1.
           + easy. }
  - destruct H.
    pose proof (Bplus_correct sb emax Hsb' Hemax' 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 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; try destruct s; destruct x; try destruct s; try easy.
        rewrite Rcompare_Gt in h3; auto.
        assert (0 < B2R (B754_finite false m0 e e0)) by
            (apply non_zero_positive_to_real; easy).
        assert (0 < B2R (B754_finite false m1 e1 e2)) by
            (apply non_zero_positive_to_real; easy).
        lra.
      * rewrite is_negative_Bsign; auto.
        destruct y; try destruct s; destruct x; try destruct s; try easy.
        rewrite Rcompare_Lt in h3; auto.
        assert (B2R (B754_finite true  m0 e e0) < 0) by
            (apply non_zero_negative_to_real; easy).
        assert (B2R (B754_finite true m1 e1 e2) < 0) by
            (apply non_zero_negative_to_real; easy).
        lra.
    + rewrite Rlt_bool_false in H1; auto.
      destruct H1 as (h1,h2).
      change (Bplus m x y) with r in h1.
      destruct (is_nan_dec r).
      destruct x; try destruct s; destruct y; try destruct s; 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_SF) 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' 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).
      { cut (not (to_real x + to_real y <> 0)).
        lra.
        intros H9.
        apply (round_plus_neq_0 radix2 fexp (round_mode m)) in H9.
        apply H9.
        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.
        apply generic_format_B2R.
        apply generic_format_B2R. }

      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 ; try destruct s; destruct y ; try destruct s;
        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 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); try destruct s; destruct 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; try easy; destruct s, s0; destruct h; easy.
  - destruct x, y; try easy; destruct s, s0; auto; easy.
  - destruct x, y; try easy; destruct s, s0; auto; easy.
  - destruct x, y; try easy; destruct s, s0; destruct h2 as [(h2,h3)|(h2,h3)]; auto; easy.
  - destruct x, y; try easy; destruct s, s0; 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' m x y h h1).
    rewrite Rlt_bool_false in H by auto.
    destruct H.
    split.

    + destruct x, y; try easy.
      * destruct s, s0, 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 s0 m0 e e0)) as (_,h3); auto.
        rewrite <-h3.
        destruct s0;[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 s;[right;split;[easy|]|left;split;[easy|]]; apply lt_finite; easy.
      * change (Bminus m (B754_finite s m0 e e0) (B754_finite s0 m1 e1 e2)) with r in H.
        pose proof (sign_FF_overflow m (Bsign (B754_finite s 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 s; 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).
          lra.
        - 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).
          lra. }

    + change (Bminus m x y) with r in H.
      assert (H':=H).
      apply (f_equal sign_SF) 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 x = true \/ Bsign x = false) by
            (destruct x ; try destruct s; 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, <- SF2R_B2SF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            now apply Pos.pow_gt_1.
        - 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 x = true \/ Bsign x = false) by
            (destruct x ; try destruct s; 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, <- SF2R_B2SF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
              now apply Pos.pow_gt_1.
          + assert (~is_nan r) by
                (destruct r; try easy; destruct n; easy).
            rewrite is_positive_Bsign; easy. }
      * assert (Bsign x = true \/ Bsign x = false) by
            (destruct x ; try destruct s; 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, <- SF2R_B2SF, H; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            now apply Pos.pow_gt_1.
        - 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, <- SF2R_B2SF, H; auto.
            *  rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
               now apply Pos.pow_gt_1.
          + easy. }
  - destruct H.
    pose proof (Bminus_correct sb emax Hsb' Hemax' 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 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; try destruct s; destruct x; try destruct s; try easy.
        rewrite Rcompare_Gt in h3; auto.
        assert (B2R (B754_finite true m0 e e0) < 0) by
            (apply non_zero_negative_to_real; easy).
        assert (0 < B2R (B754_finite false m1 e1 e2)) by
            (apply non_zero_positive_to_real; easy).
        lra.
      * rewrite is_negative_Bsign; auto.
        destruct y; try destruct s; destruct x; try destruct s; try easy.
        rewrite Rcompare_Lt in h3; auto.
        assert (0 < B2R (B754_finite false m0 e e0)) by
            (apply non_zero_positive_to_real; easy).
        assert (B2R (B754_finite true m1 e1 e2) < 0) by
            (apply non_zero_negative_to_real; easy).
        lra.
    + rewrite Rlt_bool_false in H1; auto.
      destruct H1 as (h1,h2).
      change (Bminus m x y) with r in h1.
      destruct (is_nan_dec r).
      destruct x; try destruct s; destruct y; try destruct s; 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_SF) 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' 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).
      { cut (not (to_real x - to_real y <> 0)).
        lra.
        intros H9.
        apply (round_plus_neq_0 radix2 fexp (round_mode m)) in H9.
        apply H9.
        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.
        apply generic_format_B2R.
        destruct (neg_finite y) as (_,h3); auto; rewrite <-h3.
        apply generic_format_B2R. }

      rewrite Rcompare_Eq in h; auto.
      change (Bminus m x y) with r in h.

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

      destruct x ; try destruct s; destruct y ; try destruct s;
        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 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); try destruct s; destruct 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; try destruct s; easy.
  - destruct x, y; try destruct s; try easy; contradict H2; easy.
  - destruct x, y; try destruct s0; easy.
  - destruct x, y; try destruct s0; 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' m x y).
    rewrite Rlt_bool_false in H1 by auto.
    change (Bmult m x y) with r in H1.
    assert (H1':=H1).
    apply (f_equal sign_SF) 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 x = true \/ Bsign x = false) by
          (destruct x ; try destruct s; simpl; auto).
      assert (Bsign y = true \/ Bsign y = false) by
          (destruct y; try destruct s; 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, <- SF2R_B2SF, H1; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            now apply Pos.pow_gt_1.
        - 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, <- SF2R_B2SF, H1; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            now apply Pos.pow_gt_1.
        - 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 x = true \/ Bsign x = false) by
          (destruct x ; try destruct s; simpl; auto).
      assert (Bsign y = true \/ Bsign y = false) by
          (destruct y; try destruct s; 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, <- SF2R_B2SF, H1; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            now apply Pos.pow_gt_1. }
        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, <- SF2R_B2SF, H1; auto.
          + rewrite Pos2Z.inj_sub, Pos2Z.inj_pow_pos; auto.
            now apply Pos.pow_gt_1. }
        assert (~is_nan r) by
            (destruct r; try easy; destruct n; easy).
        rewrite is_positive_Bsign, H1'; intro h; contradict h; easy. }
    * assert (Bsign x = true \/ Bsign x = false) by
          (destruct x ; try destruct s; simpl; auto).
      assert (Bsign y = true \/ Bsign y = false) by
          (destruct y; try destruct s; 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, <- SF2R_B2SF, 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.
      now apply Pos.pow_gt_1.
  - pose proof (Bmult_correct sb emax Hsb' Hemax' 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; try destruct s; destruct y; try destruct s; easy.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_SF) in H1.
      rewrite sign_FF_B2FF, sign_FF_overflow in H1.
      rewrite is_positive_Bsign; auto.
      destruct x; try destruct s; destruct y; try destruct s; easy.
  - pose proof (Bmult_correct sb emax Hsb' Hemax' 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; try destruct s; destruct y; try destruct s; easy.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_SF) in H1.
      rewrite sign_FF_B2FF, sign_FF_overflow in H1.
      rewrite is_positive_Bsign; auto.
      destruct x; try destruct s; destruct y; try destruct s; easy.
  - pose proof (Bmult_correct sb emax Hsb' Hemax' 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; try destruct s; destruct y; try destruct s; auto.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_SF) in H1.
      rewrite sign_FF_B2FF, sign_FF_overflow in H1.
      rewrite is_negative_Bsign; auto.
      destruct x; try destruct s; destruct y; try destruct s; auto.
  - pose proof (Bmult_correct sb emax Hsb' Hemax' 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; try destruct s; destruct y; try destruct s; auto.
      now apply Bool.not_true_is_false.
    + apply (f_equal sign_SF) in H1.
      rewrite sign_FF_B2FF, sign_FF_overflow in H1.
      rewrite is_negative_Bsign; auto.
      destruct x; try destruct s; destruct y; try destruct s; 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); try destruct s; destruct 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; try destruct s; easy.
  - destruct x, y; try destruct s; try easy; contradict H2; easy.
  - destruct x, y; try destruct s0; easy.
  - assert (to_real y <> 0) by (rewrite zero_to_real in H1; auto).
    pose proof (Bdiv_correct sb emax Hsb' Hemax' m x y H2).
    rewrite Rlt_bool_false in H4.
    + unfold binary_overflow in H4.
      change (Bdiv m x y) with r in H4; auto.
      destruct m; simpl in *.
      * now destruct r.
      * now destruct r.
      * destruct (xorb (Bsign x) (Bsign y)); simpl in H4. {
          split; intro.
          - destruct r; try destruct s; easy.
          - split; [destruct r; try easy; destruct b, n in H4; easy|].
            apply (f_equal (SF2R radix2)) in H4.
            rewrite SF2R_B2SF 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;
                 now apply Pos.pow_gt_1).
            rewrite <-min_real_is_F2R; assumption. }
        split; intro; [destruct r; easy|].
        destruct r; try easy.
        destruct s; try easy.
        simpl in H5; contradict H5; auto.
      * destruct (xorb (Bsign x) (Bsign y)); simpl in H4. {
        split; intro.
        - destruct r; try destruct s; easy.
        - now destruct r. }
        { split; intro.
          + split;[destruct r; easy|].
            apply (f_equal (SF2R radix2)) in H4.
            rewrite SF2R_B2SF 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;
                 now apply Pos.pow_gt_1).
            rewrite <-max_real_is_F2R; assumption.
          + destruct r; try easy; try (destruct n; easy).
            destruct s; try easy.
            simpl in H5; contradict H5; auto. }
      * { destruct (xorb (Bsign x) (Bsign y)); simpl in H4;
        split; intro.
          - destruct r; try destruct s; easy.
          - split;[destruct r; try destruct s; try easy; destruct n; easy|].
            apply (f_equal (SF2R radix2)) in H4.
            rewrite SF2R_B2SF 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;
                 now apply Pos.pow_gt_1).
            rewrite <-min_real_is_F2R; assumption.
          - split; [destruct r; try easy| ].
            apply (f_equal (SF2R radix2)) in H4.
            rewrite SF2R_B2SF 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;
                 now apply Pos.pow_gt_1).
            rewrite <-max_real_is_F2R; assumption.
          - contradict H5.
            destruct r; try destruct s; easy. }
    + clear H4.
      rewrite no_overflow_Rabs_round_emax in H3.
      apply Rge_le, Rnot_lt_ge; assumption.
  - destruct x, y; try easy.
    rewrite is_zero_B754_zero in H2; destruct H2; exists s; reflexivity.
    rewrite is_zero_B754_zero in H2; destruct H2; exists s; 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 ; try destruct s; destruct y ; try destruct s; 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; lra. }
    pose proof (Bdiv_correct sb emax Hsb' Hemax' 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_SF) in H3.
      rewrite sign_FF_B2FF, sign_FF_overflow in H3.
      rewrite is_positive_Bsign; auto.
  - destruct x ; try destruct s; destruct y ; try destruct s; 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; lra. }
    pose proof (Bdiv_correct sb emax Hsb' Hemax' 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_SF) in H3.
      rewrite sign_FF_B2FF, sign_FF_overflow in H3.
      rewrite is_positive_Bsign; auto.
  - destruct x ; try destruct s; destruct y ; try destruct s; 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; lra. }
    pose proof (Bdiv_correct sb emax Hsb' Hemax' 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_SF) in H3.
      rewrite sign_FF_B2FF, sign_FF_overflow in H3.
      rewrite is_negative_Bsign; auto.
  - destruct x; try destruct s; destruct y; try destruct s; 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; lra. }
    pose proof (Bdiv_correct sb emax Hsb' Hemax' 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_SF) 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 s;[right|left]; easy.
    destruct s;[right|left]; easy.
    contradict H; easy.
    destruct s;[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; 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 s; try easy.
        destruct x ; try destruct s; split; easy.
    * unfold Bcompare.
      destruct x, y; try easy; destruct s, s0; simpl; split; auto; easy.
    * now destruct x.
  + intros a.
    destruct y; unfold le, Bcompare in a; try easy.
    destruct x; try destruct s0; 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); try destruct s; destruct 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 ; try destruct s; easy.
  - unfold is_minus_infinity in H.
    destruct x ; try destruct s; easy.
  - destruct x ; try destruct s; try easy.
    rewrite B754_zero_to_real in H1; lra.
    rewrite B754_zero_to_real in H1; lra.
    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 s;[right|left];split;auto.
    simpl in r; unfold r; auto.
    simpl in r; unfold r; auto.
  - destruct (Bsqrt_correct sb emax Hsb' Hemax' m x) as (_,(h1,h2));
      fold r in h1, h2.
    destruct x; try easy.
    rewrite B754_zero_to_real in H1 at 1; lra.
    apply (to_real_positive _ H0) in H1.
    rewrite is_positive_Bsign in H1 by easy.
    simpl in H1.
    destruct s; 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.
  pose proof pow2sb_lt_max_int.
  split; apply IZR_le; auto with zarith.
Qed.

(* Why3 goal *)
Lemma of_int_add_exact :
  forall (m:ieee_float.RoundingMode.mode) (n:ieee_float.RoundingMode.mode)
    (i:Numbers.BinNums.Z) (j:Numbers.BinNums.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:Numbers.BinNums.Z) (j:Numbers.BinNums.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:Numbers.BinNums.Z) (j:Numbers.BinNums.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.
unfold min.
apply le_correct in 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.
apply le_correct in 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.
apply le_correct in 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.
apply le_correct in 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 = IZR (Zfloor x)).
Defined.

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

Lemma is_intR_IZR: forall i, is_intR (IZR 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; split; intro.
  exists ({| Fnum := Zfloor x; Fexp := 0 |}); simpl; auto.
  unfold F2R, Fnum, Fexp; simpl.
  rewrite Rmult_1_r; assumption.
  destruct H.
  unfold F2R in H.
  rewrite H0 in H; simpl in H.
  rewrite Rmult_1_r in H.
  apply is_intR_equiv.
  exists (Fnum f); 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.
    rewrite Zfloor_IZR; auto.
  - right; intro h; destruct h; easy.
  - right; intro h; destruct h; easy.
  - set (x := (B754_finite s m e e0)).
    unfold is_int, is_intR.
    destruct (Req_dec (to_real x) (IZR (floor (to_real x)))).
    left.
    rewrite H, Zfloor_IZR; 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.
  apply is_intR_IZR.
Qed.

Lemma B754_zero_is_int : forall {b}, (is_int (B754_zero b)).
Proof.
  split. easy.
  rewrite B754_zero_to_real.
  unfold is_intR.
  now rewrite Zfloor_IZR.
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.
  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 <- opp_IZR at 2.
  rewrite Zfloor_IZR.
  symmetry; apply opp_IZR.
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:Numbers.BinNums.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.
  apply is_intR_IZR.
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.
fold (to_real x).
case m;
  [auto|
   destruct valid_rnd_NA|
   destruct valid_rnd_UP|
   destruct valid_rnd_DN|
   destruct valid_rnd_ZR]; rewrite H0;
rewrite Zrnd_IZR; try easy.
apply valid_rnd_N.
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).
  easy.
  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, Bcompare in h2; simpl SpecFloat.SFcompare in h2.
    destruct s.
    destruct h2 as [h2|h2]. 2: easy.
    destruct (Z_lt_le_dec e 1%Z); auto.
    rewrite Zcompare_Lt in h2; auto.
    easy.
    destruct h2 as [h2|h2]. easy.
    destruct e; try easy.
    pose proof (Pos2Z.is_pos p).
    auto with zarith. }

  rewrite <- IZR_Zpower by auto with zarith.
  rewrite <- mult_IZR.
  apply is_intR_IZR.
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.
    now rewrite Zfloor_IZR.
    change (is_int (of_int RTZ (to_int m (B754_finite s 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 plus_IZR.
+ split; auto.
  rewrite max_real_int in H.
  destruct H; apply is_intR_equiv.
  exists max_int; assumption.
  exists (- max_int)%Z.
  now rewrite opp_IZR.
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 minus_IZR.
+ split; auto.
  rewrite max_real_int in H.
  destruct H; apply is_intR_equiv.
  exists max_int; assumption.
  exists (- max_int)%Z.
  now rewrite opp_IZR.
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 mult_IZR.
+ split; auto.
  rewrite max_real_int in H.
  destruct H; apply is_intR_equiv.
  exists max_int; assumption.
  exists (- max_int)%Z.
  now rewrite opp_IZR.
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 plus_IZR, mult_IZR; reflexivity.
+ split; auto.
  rewrite max_real_int in H.
  destruct H; apply is_intR_equiv.
  exists max_int; assumption.
  exists (- max_int)%Z.
  rewrite opp_IZR; 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 <- opp_IZR, Zfloor_IZR, opp_IZR.
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 <- abs_IZR, Zfloor_IZR, abs_IZR.
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) = IZR (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 s m0 e e0); fold x in h, h.
  change (to_real (of_int RTZ (to_int m x)) = IZR (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.
      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.
      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.
  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).
  apply IZR_le, Zceil_glb.
  rewrite <- (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.
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).
    apply IZR_le, Zfloor_lub.
    rewrite <- (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.
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 s; simpl; now auto); clear h.
  set (x:=B754_finite s 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 s; 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; lra.
Qed.

Lemma ceil_lb: forall x, ((IZR (ceil x) - 1) < x).
Proof.
  intro.
  case (Req_dec (IZR (Zfloor x)) x); intro.
  rewrite <-H, Zceil_IZR, H; simpl; lra.
  rewrite (Zceil_floor_neq _ H).
  rewrite plus_IZR; simpl.
  pose proof (Zfloor_lb x).
  destruct (Rle_lt_or_eq_dec _ _ H0); try easy.
  lra.
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; lra.
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 s 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); lra.

  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 (IZR (Zfloor (to_real x))) (to_real x)); intro.
  lra.

  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, plus_IZR in h; auto.
  fold (to_real x) in h.
  lra.
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 s 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); lra.
  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 (IZR (Zceil (to_real x))) (to_real x)); intro.
  lra.

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

  rewrite Zceil_floor_neq, plus_IZR in h; auto.
  rewrite Zceil_floor_neq, plus_IZR; auto.
  fold (to_real x) in h; lra.
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)).
  { apply Sterbenz.sterbenz.
    apply fexp_Valid.
    apply fexp_monotone.
    apply generic_format_B2R.
    apply generic_format_B2R.
    exact h. }
  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)).
  { replace (to_real y - to_real x) with (- (to_real x - to_real y)) by ring.
    apply generic_format_opp.
    apply Sterbenz.sterbenz.
    apply fexp_Valid.
    apply fexp_monotone.
    apply generic_format_B2R.
    apply generic_format_B2R.
    exact h. }
  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 Rgt_not_eq; lra).
    apply Rmult_le_compat_neg_l; lra.
  - 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; lra.
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)).
  split. lra.
  apply Rlt_le.
  apply Rlt_le_trans with (r2 := IZR (floor (to_real x)) + 1); auto.
  assert (1 <= IZR (floor (to_real x))).
  { pose proof (Rle_lt_trans _ _ _ h1 H0).
    rewrite <- plus_IZR in H1.
    apply lt_IZR in H1.
    apply IZR_le.
    auto with zarith. }
  lra.
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)).
  split. lra.
  destruct (Rle_lt_dec (to_real x) (-1)). lra.
  assert (IZR (floor (to_real x)) = -1).
  { assert (IZR (floor(to_real x)) < 0) by lra.
    assert (-2 < IZR (floor (to_real x))) by lra.
    apply lt_IZR in H1; apply lt_IZR in H2.
    now replace (floor (to_real x)) with (-1)%Z by lia. }
  lra.
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)).
  split. lra.
  destruct (Rle_lt_dec 1 (to_real x) ); try lra.
  assert (IZR (ceil (to_real x)) = 1).
  { assert (0 < IZR (ceil( to_real x))) by lra.
    assert (IZR (ceil(to_real x)) < 2) by lra.
    apply lt_IZR in H1; apply lt_IZR in H2.
    now replace (ceil (to_real x)) with 1%Z by lia. }
  lra.
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)).
  split. lra.
  apply Rmult_le_reg_r with (r:=2); try lra.
  replace (to_real x / 2 * 2) with (to_real x) by field.
  apply Rlt_le.
  apply Rle_lt_trans with (r2 := IZR (ceil (to_real x)) - 1); auto.
  assert (IZR (ceil (to_real x)) <= -1).
  { pose proof (Rlt_le_trans _ _ _ H h1).
    rewrite <- (minus_IZR _ 1) in H1.
    apply (lt_IZR _ (-1)) in H1.
    apply (IZR_le _ (-1)).
    auto with zarith. }
  lra.
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)).
  { apply Sterbenz.generic_format_plus_weak.
    apply fexp_Valid.
    apply fexp_monotone.
    apply generic_format_B2R.
    apply generic_format_B2R.
    exact h. }
  apply round_generic; auto.
  apply valid_rnd_round_mode.
Qed.

Lemma half_bounded: SpecFloat.bounded sb emax (shift_pos (sb_pos - 1) 1) (- sb) = true.
Proof.
  unfold SpecFloat.bounded.
  apply Bool.andb_true_iff; split.
  unfold SpecFloat.canonical_mantissa.
  apply Zeq_bool_true.
  rewrite Digits.Zpos_digits2_pos, shift_pos_correct.
  rewrite Zmult_1_r, Z.pow_pos_fold.
  rewrite Digits.Zdigits_Zpower by easy.
  rewrite Pos2Z.inj_sub by exact sb_gt_1.
  fold sb.
  unfold SpecFloat.fexp, FLT_exp, SpecFloat.emin.
  replace (sb - 1 + 1 + - sb)%Z with 0%Z by ring.
  apply Z.max_l.
  pose sb_gt_1; pose Hemax'; lia.
  apply Zle_bool_true.
  pose Hemax'; pose sb_gt_1; lia.
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 IZR_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.
  change (Z.pow_pos radix2 1)%Z with 2%Z.
  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 - IZR (floor (to_real x)) = IZR (ceil (to_real x)) - to_real x.
Proof.
  intros x h.
  destruct x; try easy.
  - rewrite B754_zero_to_real.
    rewrite Zfloor_IZR, Zceil_IZR; auto.
  - simpl.
    rewrite Zfloor_IZR, Zceil_IZR; auto.
  - set (x:=(B754_finite s 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 lra.
      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 lra.
      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).
            (apply Zfloor_imp; simpl IZR; split; lra).
        assert (ceil (to_real x) = 0%Z) by
            (apply Zceil_imp; simpl IZR; split; lra).

        revert h.
        rewrite (to_real_roundToIntegral RTP) by easy.
        unfold to_int.
        fold (to_real x).
        rewrite H1.
        rewrite Rminus_0_l.
        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.
             rewrite <- opp_IZR; simpl IZR.
             rewrite Rabs_pos_eq, Rabs_left, Rabs_pos_eq, Rmin_left ; lra. }
           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.
           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.
           lra. }
      * assert (floor (to_real x) = 0%Z) by
            (apply Zfloor_imp; simpl IZR; split; lra).
        assert (ceil (to_real x) = 0%Z) by
            (apply Zceil_imp; simpl IZR; split; lra).
        rewrite H0, H1, H; auto.

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

        revert h.
        rewrite (to_real_roundToIntegral RTN) by easy.
        unfold to_int.
        fold (to_real x).
        rewrite H.
        replace (to_real x - 0) with (to_real x) by (simpl IZR ; 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.
             rewrite Rabs_pos_eq, Rabs_pos_eq, Rabs_left, Rmin_right; lra. }
           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.
           intros.
           lra. }
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 s 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 H', Zfloor_IZR; reflexivity.

  unfold Znearest.
  rewrite Rcompare_Eq.
  rewrite Zle_bool_false; auto.
  apply lt_IZR.
  apply Rle_lt_trans with (r2:=to_real x).
  apply Zfloor_lb.
  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 plus_IZR in h.
  lra.

  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 s 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 H', Zceil_IZR; reflexivity.

  unfold Znearest.
  rewrite Rcompare_Eq.
  rewrite Zle_bool_true; auto.
  apply non_zero_positive_to_real in h'; try easy.
  apply Zfloor_lub.
  lra.
  unfold is_zero.
  unfold eq. simpl.
  now destruct s.

  rewrite Zceil_floor_neq in h.
  rewrite plus_IZR in h.
  lra.

  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 s 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:Numbers.BinNums.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.