proposition: Lemma SF2B'_B2SF : forall {prec emax} (x : binary_float prec emax), SF2B' (B2SF x) = x.
proof: Proof. intros prec emax [s|s| |s m e H] ; try easy. apply B2SF_inj. simpl. generalize (eq_refl (bounded prec emax m e)). pattern (bounded prec emax m e) at 2 3. apply eq_sym in H. now elim H. Qed.
imports: Coq(ZArith SpecFloat) Flocq(BinarySingleNaN)