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

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

Import Flocq.Core.Fcore.
Import Flocq.Appli.Fappli_IEEE.
Import ieee_float.RoundingMode.
Import ieee_float.GenericFloat.

(* Why3 goal *)
Definition t : Type.
Proof.
  exact (t 8 24).
Defined.

(* Why3 goal *)
Definition t'real: t -> R.
Proof.
  apply B2R.
Defined.

(* Why3 goal *)
Definition t'isFinite: t -> Prop.
Proof.
  apply is_finite.
Defined.

(* Why3 goal *)
Lemma t'axiom : forall (x:t), (t'isFinite x) ->
  (((-(16777215 * 20282409603651670423947251286016)%R)%R <= (t'real x))%R /\
  ((t'real x) <= (16777215 * 20282409603651670423947251286016)%R)%R).
Proof.
intros x _.
apply Rabs_le_inv.
change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 24 - 1) (127 - 23)))%R.
destruct x as [s|s|s|s m e H] ;
  try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0_compat).
simpl.
rewrite <- F2R_Zabs.
rewrite abs_cond_Zopp.
apply andb_prop in H.
destruct H as [H1 H2].
apply Zeq_bool_eq in H1.
apply Zle_bool_imp_le in H2.
rewrite Fcore_digits.Zpos_digits2_pos in H1.
apply Rmult_le_compat.
now apply (Z2R_le 0).
apply bpow_ge_0.
apply Z2R_le.
apply (Z.lt_le_pred (Zabs (Zpos m)) (Zpower radix2 24)).
apply Fcore_digits.Zpower_gt_Zdigits.
revert H1.
generalize (Fcore_digits.Zdigits radix2 (Z.pos m)).
unfold FLT_exp, sb.
intros ; zify ; omega.
now apply bpow_le.
Qed.

(* Why3 goal *)
Definition zeroF: t.
Proof.
  apply zeroF.
Defined.

(* Why3 goal *)
Definition add: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  now apply add.
Defined.

(* Why3 goal *)
Definition sub: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  now apply sub.
Defined.

(* Why3 goal *)
Definition mul: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  now apply mul.
Defined.

(* Why3 goal *)
Definition div: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  now apply div.
Defined.

(* Why3 goal *)
Definition abs: t -> t.
Proof.
  apply abs.
Defined.

(* Why3 goal *)
Definition neg: t -> t.
Proof.
  apply neg.
Defined.

(* Why3 goal *)
Definition fma: ieee_float.RoundingMode.mode -> t -> t -> t -> t.
Proof.
  now apply fma.
Defined.

(* Why3 goal *)
Definition sqrt: ieee_float.RoundingMode.mode -> t -> t.
Proof.
  now apply GenericFloat.sqrt.
Defined.

(* Why3 goal *)
Definition roundToIntegral: ieee_float.RoundingMode.mode -> t -> t.
Proof.
  now apply roundToIntegral.
Defined.

(* Why3 goal *)
Definition min: t -> t -> t.
Proof.
  now apply min.
Defined.

(* Why3 goal *)
Definition max: t -> t -> t.
Proof.
  now apply max.
Defined.

(* Why3 goal *)
Definition le: t -> t -> Prop.
Proof.
  apply le.
Defined.

(* Why3 goal *)
Definition lt: t -> t -> Prop.
Proof.
  apply lt.
Defined.

(* Why3 goal *)
Definition eq: t -> t -> Prop.
Proof.
  apply eq.
Defined.

(* Why3 goal *)
Definition is_normal: t -> Prop.
Proof.
  apply is_normal.
Defined.

(* Why3 goal *)
Definition is_subnormal: t -> Prop.
Proof.
  apply is_subnormal.
Defined.

(* Why3 goal *)
Definition is_zero: t -> Prop.
Proof.
  apply is_zero.
Defined.

(* Why3 goal *)
Definition is_infinite: t -> Prop.
Proof.
  apply is_infinite.
Defined.

(* Why3 goal *)
Definition is_nan: t -> Prop.
Proof.
  apply is_nan.
Defined.

(* Why3 goal *)
Definition is_positive: t -> Prop.
Proof.
  apply is_positive.
Defined.

(* Why3 goal *)
Definition is_negative: t -> Prop.
Proof.
  apply is_negative.
Defined.

(* 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 := (t'isFinite x) \/ (is_infinite x).

(* Why3 goal *)
Lemma is_not_nan1 : forall (x:t), (is_not_nan x) <-> ~ (is_nan x).
Proof.
  apply is_not_nan1.
Qed.

(* Why3 goal *)
Lemma is_not_finite : forall (x:t), (~ (t'isFinite x)) <-> ((is_infinite
  x) \/ (is_nan x)).
Proof.
  apply is_not_finite.
Qed.

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

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

(* Why3 goal *)
Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((t'isFinite x) /\
  ((t'real x) = 0%R)).
Proof.
  apply zero_to_real.
Qed.

(* Why3 goal *)
Definition of_int: ieee_float.RoundingMode.mode -> Z -> t.
Proof.
  now apply z_to_fp.
Defined.

(* Why3 goal *)
Definition to_int: ieee_float.RoundingMode.mode -> t -> Z.
Proof.
  now apply fp_to_z.
Defined.

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

(* Why3 goal *)
Definition round: ieee_float.RoundingMode.mode -> R -> R.
Proof.
  apply (round 8 24).
Defined.

Lemma max_real_cst :
  max_real 8 24 = (33554430 * 10141204801825835211973625643008)%R.
Proof.
  change (33554430 * 10141204801825835211973625643008)%R
    with (F2R (Float radix2 (16777215 * Zpower radix2 (104 - 103)) 103)).
  rewrite <- F2R_change_exp by easy.
  now rewrite <- max_real_is_F2R.
Qed.

(* Why3 goal *)
Definition max_int: Z.
Proof.
  exact (33554430 * 10141204801825835211973625643008)%Z.
Defined.

(* Why3 goal *)
Lemma max_real_int : ((33554430 * 10141204801825835211973625643008)%R = (BuiltIn.IZR max_int)).
Proof.
  unfold max_int.
  now rewrite mult_IZR, <- !Z2R_IZR.
Qed.

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

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

(* Why3 goal *)
Lemma is_finite : forall (x:t), (t'isFinite x) -> (in_range (t'real x)).
Proof.
  unfold t'isFinite, in_range.
  intros x Hx.
  rewrite <- max_real_cst.
  now apply is_finite1.
Qed.

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

(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:ieee_float.RoundingMode.mode)
  (x:R), (in_range x) -> (no_overflow m x).
Proof.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply (Bounded_real_no_overflow 8 24).
Qed.

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

(* Why3 goal *)
Lemma Round_idempotent : forall (m1:ieee_float.RoundingMode.mode)
  (m2:ieee_float.RoundingMode.mode) (x:R), ((round m1 (round m2
  x)) = (round m2 x)).
Proof.
  apply Round_idempotent.
Qed.

(* Why3 goal *)
Lemma Round_to_real : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (t'isFinite x) -> ((round m (t'real x)) = (t'real x)).
Proof.
  apply Round_to_real.
Qed.

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

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

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

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

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

(* Why3 goal *)
Lemma Exact_rounding_for_integers : forall (m:ieee_float.RoundingMode.mode)
  (i:Z), (in_safe_int_range i) -> ((round m
  (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
  intros m i h1.
  now apply Exact_rounding_for_integers.
Qed.

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

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

(* Why3 goal *)
Lemma feq_eq : forall (x:t) (y:t), (t'isFinite x) -> ((t'isFinite y) ->
  ((~ (is_zero x)) -> ((eq x y) -> (x = y)))).
Proof.
  apply feq_eq.
Qed.

(* Why3 goal *)
Lemma eq_feq : forall (x:t) (y:t), (t'isFinite x) -> ((t'isFinite y) ->
  ((x = y) -> (eq x y))).
Proof.
  apply eq_feq.
Qed.

(* Why3 goal *)
Lemma eq_refl : forall (x:t), (t'isFinite x) -> (eq x x).
Proof.
  apply eq_refl.
Qed.

(* Why3 goal *)
Lemma eq_sym : forall (x:t) (y:t), (eq x y) -> (eq y x).
Proof.
  apply eq_sym.
Qed.

(* Why3 goal *)
Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x
  z)).
Proof.
  apply eq_trans.
Qed.

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

(* Why3 goal *)
Lemma eq_to_real_finite : forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite
  y)) -> ((eq x y) <-> ((t'real x) = (t'real y))).
Proof.
  apply eq_to_real_finite.
Qed.

(* Why3 goal *)
Lemma eq_special : forall (x:t) (y:t), (eq x y) -> ((is_not_nan x) /\
  ((is_not_nan y) /\ (((t'isFinite x) /\ (t'isFinite y)) \/ ((is_infinite
  x) /\ ((is_infinite y) /\ (same_sign x y)))))).
Proof.
  apply eq_special.
Qed.

(* Why3 goal *)
Lemma lt_finite : forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite y)) ->
  ((lt x y) <-> ((t'real x) < (t'real y))%R).
Proof.
  apply lt_finite.
Qed.

(* Why3 goal *)
Lemma le_finite : forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite y)) ->
  ((le x y) <-> ((t'real x) <= (t'real y))%R).
Proof.
  apply le_finite.
Qed.

(* Why3 goal *)
Lemma le_lt_trans : forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x
  z).
Proof.
  apply le_lt_trans.
Qed.

(* Why3 goal *)
Lemma lt_le_trans : forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x
  z).
Proof.
  apply lt_le_trans.
Qed.

(* Why3 goal *)
Lemma le_ge_asym : forall (x:t) (y:t), ((le x y) /\ (le y x)) -> (eq x y).
Proof.
  apply le_ge_asym.
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.
  apply not_lt_ge.
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.
 apply not_gt_le.
Qed.

(* Why3 goal *)
Lemma le_special : forall (x:t) (y:t), (le x y) -> (((t'isFinite x) /\
  (t'isFinite y)) \/ (((is_minus_infinity x) /\ (is_not_nan y)) \/
  ((is_not_nan x) /\ (is_plus_infinity y)))).
Proof.
  apply le_special.
Qed.

(* Why3 goal *)
Lemma lt_special : forall (x:t) (y:t), (lt x y) -> (((t'isFinite x) /\
  (t'isFinite 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.
  apply lt_special.
Qed.

(* Why3 goal *)
Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) ->
  (t'isFinite y)).
Proof.
  apply lt_lt_finite.
Qed.

(* Why3 goal *)
Lemma positive_to_real : forall (x:t), (t'isFinite x) -> ((is_positive x) ->
  (0%R <= (t'real x))%R).
Proof.
  apply positive_to_real.
Qed.

(* Why3 goal *)
Lemma to_real_positive : forall (x:t), (t'isFinite x) ->
  ((0%R < (t'real x))%R -> (is_positive x)).
Proof.
  apply to_real_positive.
Qed.

(* Why3 goal *)
Lemma negative_to_real : forall (x:t), (t'isFinite x) -> ((is_negative x) ->
  ((t'real x) <= 0%R)%R).
Proof.
  apply negative_to_real.
Qed.

(* Why3 goal *)
Lemma to_real_negative : forall (x:t), (t'isFinite x) ->
  (((t'real x) < 0%R)%R -> (is_negative x)).
Proof.
  apply to_real_negative.
Qed.

(* Why3 goal *)
Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\
  (is_negative x)).
Proof.
  apply negative_xor_positive.
Qed.

(* Why3 goal *)
Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive
  x) \/ (is_negative x)).
Proof.
  apply negative_or_positive.
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.
  apply diff_sign_trans.
Qed.

(* Why3 goal *)
Lemma diff_sign_product : forall (x:t) (y:t), ((t'isFinite x) /\ ((t'isFinite
  y) /\ (((t'real x) * (t'real y))%R < 0%R)%R)) -> (diff_sign x y).
Proof.
  apply diff_sign_product.
Qed.

(* Why3 goal *)
Lemma same_sign_product : forall (x:t) (y:t), ((t'isFinite x) /\ ((t'isFinite
  y) /\ (same_sign x y))) -> (0%R <= ((t'real x) * (t'real y))%R)%R.
Proof.
  apply same_sign_product.
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) -> ((t'isFinite x) /\
      ((t'real x) = (33554430 * 10141204801825835211973625643008)%R))) /\
      ((~ (is_positive x)) -> (is_infinite x))
  | ieee_float.RoundingMode.RTP => ((is_positive x) -> (is_infinite x)) /\
      ((~ (is_positive x)) -> ((t'isFinite x) /\
      ((t'real x) = (-(33554430 * 10141204801825835211973625643008)%R)%R)))
  | ieee_float.RoundingMode.RTZ => ((is_positive x) -> ((t'isFinite x) /\
      ((t'real x) = (33554430 * 10141204801825835211973625643008)%R))) /\
      ((~ (is_positive x)) -> ((t'isFinite x) /\
      ((t'real x) = (-(33554430 * 10141204801825835211973625643008)%R)%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),
  (t'isFinite x) -> ((t'isFinite y) -> ((no_overflow m
  ((t'real x) + (t'real y))%R) -> ((t'isFinite (add m x y)) /\
  ((t'real (add m x y)) = (round m ((t'real x) + (t'real y))%R))))).
Proof.
  intros m x y h1 h2 h3.
  apply add_finite ; try easy.
  unfold no_overflow, in_range in h3.
  now rewrite <- max_real_cst in h3.
Qed.

(* Why3 goal *)
Lemma add_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite (add m x y)) -> ((t'isFinite x) /\ (t'isFinite y)).
Proof.
  apply add_finite_rev.
Qed.

(* Why3 goal *)
Lemma add_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> ((t'isFinite (add m x y)) ->
  ((no_overflow m ((t'real x) + (t'real y))%R) /\ ((t'real (add m x
  y)) = (round m ((t'real x) + (t'real y))%R)))).
Proof.
  intros m x y h1 h2.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply add_finite_rev_n.
Qed.

(* Why3 goal *)
Lemma sub_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite x) -> ((t'isFinite y) -> ((no_overflow m
  ((t'real x) - (t'real y))%R) -> ((t'isFinite (sub m x y)) /\
  ((t'real (sub m x y)) = (round m ((t'real x) - (t'real y))%R))))).
Proof.
  intros m x y h1 h2 h3.
  apply sub_finite ; try easy.
  unfold no_overflow, in_range in h3.
  now rewrite <- max_real_cst in h3.
Qed.

(* Why3 goal *)
Lemma sub_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite (sub m x y)) -> ((t'isFinite x) /\ (t'isFinite y)).
Proof.
  apply sub_finite_rev.
Qed.

(* Why3 goal *)
Lemma sub_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> ((t'isFinite (sub m x y)) ->
  ((no_overflow m ((t'real x) - (t'real y))%R) /\ ((t'real (sub m x
  y)) = (round m ((t'real x) - (t'real y))%R)))).
Proof.
  intros m x y h1 h2.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply sub_finite_rev_n.
Qed.

(* Why3 goal *)
Lemma mul_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite x) -> ((t'isFinite y) -> ((no_overflow m
  ((t'real x) * (t'real y))%R) -> ((t'isFinite (mul m x y)) /\
  ((t'real (mul m x y)) = (round m ((t'real x) * (t'real y))%R))))).
Proof.
  intros m x y h1 h2 h3.
  apply mul_finite ; try easy.
  unfold no_overflow, in_range in h3.
  now rewrite <- max_real_cst in h3.
Qed.

(* Why3 goal *)
Lemma mul_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite (mul m x y)) -> ((t'isFinite x) /\ (t'isFinite y)).
Proof.
  apply mul_finite_rev.
Qed.

(* Why3 goal *)
Lemma mul_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> ((t'isFinite (mul m x y)) ->
  ((no_overflow m ((t'real x) * (t'real y))%R) /\ ((t'real (mul m x
  y)) = (round m ((t'real x) * (t'real y))%R)))).
Proof.
  intros m x y h1 h2.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply mul_finite_rev_n.
Qed.

(* Why3 goal *)
Lemma div_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite x) -> ((t'isFinite y) -> ((~ (is_zero y)) -> ((no_overflow m
  ((t'real x) / (t'real y))%R) -> ((t'isFinite (div m x y)) /\
  ((t'real (div m x y)) = (round m ((t'real x) / (t'real y))%R)))))).
Proof.
  intros m x y h1 h2 h3 h4.
  apply div_finite ; try easy.
  unfold no_overflow, in_range in h4.
  now rewrite <- max_real_cst in h4.
Qed.

(* Why3 goal *)
Lemma div_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite (div m x y)) -> (((t'isFinite x) /\ ((t'isFinite y) /\
  ~ (is_zero y))) \/ ((t'isFinite x) /\ ((is_infinite y) /\ ((t'real (div m x
  y)) = 0%R)))).
Proof.
  apply div_finite_rev.
Qed.

(* Why3 goal *)
Lemma div_finite_rev_n : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> ((t'isFinite (div m x y)) ->
  ((t'isFinite y) -> ((no_overflow m ((t'real x) / (t'real y))%R) /\
  ((t'real (div m x y)) = (round m ((t'real x) / (t'real y))%R))))).
Proof.
  intros m x y h1 h2 h3.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply div_finite_rev_n.
Qed.

(* Why3 goal *)
Lemma neg_finite : forall (x:t), (t'isFinite x) -> ((t'isFinite (neg x)) /\
  ((t'real (neg x)) = (-(t'real x))%R)).
Proof.
  apply neg_finite.
Qed.

(* Why3 goal *)
Lemma neg_finite_rev : forall (x:t), (t'isFinite (neg x)) -> ((t'isFinite
  x) /\ ((t'real (neg x)) = (-(t'real x))%R)).
Proof.
  apply neg_finite_rev.
Qed.

(* Why3 goal *)
Lemma abs_finite : forall (x:t), (t'isFinite x) -> ((t'isFinite (abs x)) /\
  (((t'real (abs x)) = (Reals.Rbasic_fun.Rabs (t'real x))) /\ (is_positive
  (abs x)))).
Proof.
  apply abs_finite.
Qed.

(* Why3 goal *)
Lemma abs_finite_rev : forall (x:t), (t'isFinite (abs x)) -> ((t'isFinite
  x) /\ ((t'real (abs x)) = (Reals.Rbasic_fun.Rabs (t'real x)))).
Proof.
  apply abs_finite_rev.
Qed.

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

(* Why3 goal *)
Lemma fma_finite : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t) (z:t),
  (t'isFinite x) -> ((t'isFinite y) -> ((t'isFinite z) -> ((no_overflow m
  (((t'real x) * (t'real y))%R + (t'real z))%R) -> ((t'isFinite (fma m x y
  z)) /\ ((t'real (fma m x y z)) = (round m
  (((t'real x) * (t'real y))%R + (t'real z))%R)))))).
Proof.
  intros m x y z h1 h2 h3 h4.
  apply fma_finite ; try easy.
  unfold no_overflow, in_range in h4.
  now rewrite <- max_real_cst in h4.
Qed.

(* Why3 goal *)
Lemma fma_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t)
  (z:t), (t'isFinite (fma m x y z)) -> ((t'isFinite x) /\ ((t'isFinite y) /\
  (t'isFinite z))).
Proof.
  apply fma_finite_rev.
Qed.

(* 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) -> ((t'isFinite (fma m x y
  z)) -> ((no_overflow m (((t'real x) * (t'real y))%R + (t'real z))%R) /\
  ((t'real (fma m x y z)) = (round m
  (((t'real x) * (t'real y))%R + (t'real z))%R)))).
Proof.
  intros m x y z h1 h2.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply fma_finite_rev_n.
Qed.

(* Why3 goal *)
Lemma sqrt_finite : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (t'isFinite x) -> ((0%R <= (t'real x))%R -> ((t'isFinite (sqrt m x)) /\
  ((t'real (sqrt m x)) = (round m (Reals.R_sqrt.sqrt (t'real x)))))).
Proof.
  apply sqrt_finite.
Qed.

(* Why3 goal *)
Lemma sqrt_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (t'isFinite (sqrt m x)) -> ((t'isFinite x) /\ ((0%R <= (t'real x))%R /\
  ((t'real (sqrt m x)) = (round m (Reals.R_sqrt.sqrt (t'real x)))))).
Proof.
  apply sqrt_finite_rev.
Qed.

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

(* 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)) /\
  ((((t'isFinite x) /\ (is_infinite y)) -> ((is_infinite r) /\ (same_sign r
  y))) /\ ((((is_infinite x) /\ (t'isFinite 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)) /\ ((((t'isFinite
  x) /\ ((t'isFinite y) /\ ~ (no_overflow m ((t'real x) + (t'real y))%R))) ->
  ((same_sign_real r ((t'real x) + (t'real y))%R) /\ (overflow_value m
  r))) /\ (((t'isFinite x) /\ (t'isFinite 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 no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply add_special.
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)) /\
  ((((t'isFinite x) /\ (is_infinite y)) -> ((is_infinite r) /\ (diff_sign r
  y))) /\ ((((is_infinite x) /\ (t'isFinite 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))) /\ ((((t'isFinite x) /\
  ((t'isFinite y) /\ ~ (no_overflow m ((t'real x) - (t'real y))%R))) ->
  ((same_sign_real r ((t'real x) - (t'real y))%R) /\ (overflow_value m
  r))) /\ (((t'isFinite x) /\ (t'isFinite 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 no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply sub_special.
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)) /\ ((((t'isFinite x) /\
  ((is_infinite y) /\ ~ (is_zero x))) -> (is_infinite r)) /\ ((((is_infinite
  x) /\ (is_zero y)) -> (is_nan r)) /\ ((((is_infinite x) /\ ((t'isFinite
  y) /\ ~ (is_zero y))) -> (is_infinite r)) /\ ((((is_infinite x) /\
  (is_infinite y)) -> (is_infinite r)) /\ ((((t'isFinite x) /\ ((t'isFinite
  y) /\ ~ (no_overflow m ((t'real x) * (t'real y))%R))) -> (overflow_value m
  r)) /\ ((~ (is_nan r)) -> (product_sign r x y))))))))).
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply mul_special.
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)) /\
  ((((t'isFinite x) /\ (is_infinite y)) -> (is_zero r)) /\ ((((is_infinite
  x) /\ (t'isFinite y)) -> (is_infinite r)) /\ ((((is_infinite x) /\
  (is_infinite y)) -> (is_nan r)) /\ ((((t'isFinite x) /\ ((t'isFinite y) /\
  ((~ (is_zero y)) /\ ~ (no_overflow m ((t'real x) / (t'real y))%R)))) ->
  (overflow_value m r)) /\ ((((t'isFinite 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 no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply div_special.
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.
  apply neg_special.
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.
  apply abs_special.
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)) /\ ((((t'isFinite x) /\
  ((~ (is_zero x)) /\ ((is_infinite y) /\ (t'isFinite z)))) -> ((is_infinite
  r) /\ (product_sign r x y))) /\ ((((t'isFinite 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) /\ ((t'isFinite y) /\ ((~ (is_zero
  y)) /\ (t'isFinite z)))) -> ((is_infinite r) /\ (product_sign r x y))) /\
  ((((is_infinite x) /\ ((t'isFinite 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) /\ (t'isFinite z))) -> ((is_infinite r) /\ (product_sign r
  x y))) /\ ((((t'isFinite x) /\ ((t'isFinite 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)))) /\ ((((t'isFinite x) /\ ((t'isFinite y) /\ ((t'isFinite z) /\
  ~ (no_overflow m (((t'real x) * (t'real y))%R + (t'real z))%R)))) ->
  ((same_sign_real r (((t'real x) * (t'real y))%R + (t'real z))%R) /\
  (overflow_value m r))) /\ (((t'isFinite x) /\ ((t'isFinite y) /\
  (t'isFinite z))) -> (((product_sign z x y) -> (same_sign r z)) /\
  ((~ (product_sign z x y)) ->
  (((((t'real x) * (t'real y))%R + (t'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.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply fma_special.
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)) /\
  ((((t'isFinite x) /\ ((t'real x) < 0%R)%R) -> (is_nan r)) /\ (((is_zero
  x) -> (same_sign r x)) /\ (((t'isFinite x) /\ (0%R < (t'real x))%R) ->
  (is_positive r))))))).
Proof.
  apply sqrt_special.
Qed.

(* Why3 goal *)
Lemma of_int_add_exact : forall (m:ieee_float.RoundingMode.mode)
  (n:ieee_float.RoundingMode.mode) (i:Z) (j:Z), (in_safe_int_range i) ->
  ((in_safe_int_range j) -> ((in_safe_int_range (i + j)%Z) -> (eq (of_int m
  (i + j)%Z) (add n (of_int m i) (of_int m j))))).
Proof.
  intros m n i j h1 h2 h3.
  now apply of_int_add_exact.
Qed.

(* Why3 goal *)
Lemma of_int_sub_exact : forall (m:ieee_float.RoundingMode.mode)
  (n:ieee_float.RoundingMode.mode) (i:Z) (j:Z), (in_safe_int_range i) ->
  ((in_safe_int_range j) -> ((in_safe_int_range (i - j)%Z) -> (eq (of_int m
  (i - j)%Z) (sub n (of_int m i) (of_int m j))))).
Proof.
  intros m n i j h1 h2 h3.
  now apply of_int_sub_exact.
Qed.

(* Why3 goal *)
Lemma of_int_mul_exact : forall (m:ieee_float.RoundingMode.mode)
  (n:ieee_float.RoundingMode.mode) (i:Z) (j:Z), (in_safe_int_range i) ->
  ((in_safe_int_range j) -> ((in_safe_int_range (i * j)%Z) -> (eq (of_int m
  (i * j)%Z) (mul n (of_int m i) (of_int m j))))).
Proof.
  intros m n i j h1 h2 h3.
  now apply of_int_mul_exact.
Qed.

(* Why3 goal *)
Lemma Min_r : forall (x:t) (y:t), (le y x) -> (eq (min x y) y).
Proof.
  apply Min_r.
Qed.

(* Why3 goal *)
Lemma Min_l : forall (x:t) (y:t), (le x y) -> (eq (min x y) x).
Proof.
  apply Min_l.
Qed.

(* Why3 goal *)
Lemma Max_r : forall (x:t) (y:t), (le y x) -> (eq (max x y) x).
Proof.
  apply Max_r.
Qed.

(* Why3 goal *)
Lemma Max_l : forall (x:t) (y:t), (le x y) -> (eq (max x y) y).
Proof.
  apply Max_l.
Qed.

(* Why3 goal *)
Definition is_int: t -> Prop.
Proof.
  apply is_int.
Defined.

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

(* Why3 goal *)
Lemma of_int_is_int : forall (m:ieee_float.RoundingMode.mode) (x:Z),
  (in_int_range x) -> (is_int (of_int m x)).
Proof.
  intros m x h1.
  now apply of_int_is_int.
Qed.

(* Why3 goal *)
Lemma big_float_is_int : forall (m:ieee_float.RoundingMode.mode) (i:t),
  (t'isFinite i) -> (((le i (neg (of_int m 16777216%Z))) \/ (le (of_int m
  16777216%Z) i)) -> (is_int i)).
Proof.
  now apply big_float_is_int.
Qed.

(* Why3 goal *)
Lemma roundToIntegral_is_int : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (t'isFinite x) -> (is_int (roundToIntegral m x)).
Proof.
  now apply roundToIntegral_is_int.
Qed.

(* Why3 goal *)
Lemma eq_is_int : forall (x:t) (y:t), (eq x y) -> ((is_int x) -> (is_int y)).
Proof.
  apply eq_is_int.
Qed.

(* Why3 goal *)
Lemma add_int : forall (x:t) (y:t) (m:ieee_float.RoundingMode.mode), (is_int
  x) -> ((is_int y) -> ((t'isFinite (add m x y)) -> (is_int (add m x y)))).
Proof.
  apply add_int.
Qed.

(* Why3 goal *)
Lemma sub_int : forall (x:t) (y:t) (m:ieee_float.RoundingMode.mode), (is_int
  x) -> ((is_int y) -> ((t'isFinite (sub m x y)) -> (is_int (sub m x y)))).
Proof.
  apply sub_int.
Qed.

(* Why3 goal *)
Lemma mul_int : forall (x:t) (y:t) (m:ieee_float.RoundingMode.mode), (is_int
  x) -> ((is_int y) -> ((t'isFinite (mul m x y)) -> (is_int (mul m x y)))).
Proof.
  apply mul_int.
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) -> ((t'isFinite (fma m x y z)) ->
  (is_int (fma m x y z))))).
Proof.
  now apply fma_int.
Qed.

(* Why3 goal *)
Lemma neg_int : forall (x:t), (is_int x) -> (is_int (neg x)).
Proof.
  apply neg_int.
Qed.

(* Why3 goal *)
Lemma abs_int : forall (x:t), (is_int x) -> (is_int (abs x)).
Proof.
  apply abs_int.
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.
  now apply is_int_of_int.
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.
  now apply is_int_to_int.
Qed.

(* Why3 goal *)
Lemma is_int_is_finite : forall (x:t), (is_int x) -> (t'isFinite x).
Proof.
  apply is_int_is_finite.
Qed.

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

(* Why3 goal *)
Lemma truncate_int : forall (m:ieee_float.RoundingMode.mode) (i:t), (is_int
  i) -> (eq (roundToIntegral m i) i).
Proof.
  now apply truncate_int.
Qed.

(* Why3 goal *)
Lemma truncate_neg : forall (x:t), (t'isFinite x) -> ((is_negative x) ->
  ((roundToIntegral ieee_float.RoundingMode.RTZ
  x) = (roundToIntegral ieee_float.RoundingMode.RTP x))).
Proof.
  apply truncate_neg.
Qed.

(* Why3 goal *)
Lemma truncate_pos : forall (x:t), (t'isFinite x) -> ((is_positive x) ->
  ((roundToIntegral ieee_float.RoundingMode.RTZ
  x) = (roundToIntegral ieee_float.RoundingMode.RTN x))).
Proof.
  apply truncate_pos.
Qed.

(* Why3 goal *)
Lemma ceil_le : forall (x:t), (t'isFinite x) -> (le x
  (roundToIntegral ieee_float.RoundingMode.RTP x)).
Proof.
  now apply ceil_le.
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.
  now apply ceil_lest.
Qed.

(* Why3 goal *)
Lemma ceil_to_real : forall (x:t), (t'isFinite x) ->
  ((t'real (roundToIntegral ieee_float.RoundingMode.RTP
  x)) = (BuiltIn.IZR (real.Truncate.ceil (t'real x)))).
Proof.
  now apply ceil_to_real.
Qed.

(* Why3 goal *)
Lemma ceil_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (t'isFinite x) -> ((to_int m (roundToIntegral ieee_float.RoundingMode.RTP
  x)) = (real.Truncate.ceil (t'real x))).
Proof.
  now apply ceil_to_int.
Qed.

(* Why3 goal *)
Lemma floor_le : forall (x:t), (t'isFinite x) -> (le
  (roundToIntegral ieee_float.RoundingMode.RTN x) x).
Proof.
  now apply floor_le.
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.
  now apply floor_lest.
Qed.

(* Why3 goal *)
Lemma floor_to_real : forall (x:t), (t'isFinite x) ->
  ((t'real (roundToIntegral ieee_float.RoundingMode.RTN
  x)) = (BuiltIn.IZR (real.Truncate.floor (t'real x)))).
Proof.
  now apply floor_to_real.
Qed.

(* Why3 goal *)
Lemma floor_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t),
  (t'isFinite x) -> ((to_int m (roundToIntegral ieee_float.RoundingMode.RTN
  x)) = (real.Truncate.floor (t'real x))).
Proof.
  now apply floor_to_int.
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.
  apply RNA_down.
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.
  apply RNA_up.
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.
  apply RNA_down_tie.
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.
  apply RNA_up_tie.
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.
  now apply to_int_roundToIntegral.
Qed.

(* Why3 goal *)
Lemma to_int_monotonic : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite x) -> ((t'isFinite y) -> ((le x y) -> ((to_int m
  x) <= (to_int m y))%Z)).
Proof.
  apply to_int_monotonic.
Qed.

(* Why3 goal *)
Lemma to_int_of_int : forall (m:ieee_float.RoundingMode.mode) (i:Z),
  (in_safe_int_range i) -> ((to_int m (of_int m i)) = i).
Proof.
  intros m i h1.
  now apply to_int_of_int.
Qed.

(* Why3 goal *)
Lemma eq_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite x) -> ((eq x y) -> ((to_int m x) = (to_int m y))).
Proof.
  apply eq_to_int.
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.
  apply neg_to_int.
Qed.

(* Why3 goal *)
Lemma roundToIntegral_is_finite : forall (m:ieee_float.RoundingMode.mode)
  (x:t), (t'isFinite x) -> (t'isFinite (roundToIntegral m x)).
Proof.
  now apply roundToIntegral_is_finite.
Qed.

(* Why3 goal *)
Lemma round_bound_ne : forall (x:R), (no_overflow ieee_float.RoundingMode.RNE
  x) ->
  ((((x - ((1 / 16777216)%R * (Reals.Rbasic_fun.Rabs x))%R)%R - (1 / 1427247692705959881058285969449495136382746624)%R)%R <= (round ieee_float.RoundingMode.RNE
  x))%R /\ ((round ieee_float.RoundingMode.RNE
  x) <= ((x + ((1 / 16777216)%R * (Reals.Rbasic_fun.Rabs x))%R)%R + (1 / 1427247692705959881058285969449495136382746624)%R)%R)%R).
intros x h1.
Admitted.

(* Why3 goal *)
Lemma round_bound : forall (m:ieee_float.RoundingMode.mode) (x:R),
  (no_overflow m x) ->
  ((((x - ((1 / 8388608)%R * (Reals.Rbasic_fun.Rabs x))%R)%R - (1 / 713623846352979940529142984724747568191373312)%R)%R <= (round m
  x))%R /\ ((round m
  x) <= ((x + ((1 / 8388608)%R * (Reals.Rbasic_fun.Rabs x))%R)%R + (1 / 713623846352979940529142984724747568191373312)%R)%R)%R).
intros m x h1.
Admitted.