proposition: Lemma binary_normalize_equiv m e szero : SpecFloat.binary_normalize prec emax m e szero = B2SF (binary_normalize prec emax Hprec Hmax mode_NE m e szero).
proof: Proof. case m as [ | p | p]. - now simpl. - simpl; rewrite B2SF_SF2B; apply binary_round_equiv. - simpl; rewrite B2SF_SF2B; apply binary_round_equiv. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN