proposition: Theorem Prim2SF_inj : forall x y, Prim2SF x = Prim2SF y -> x = y.
proof: Proof. intros. rewrite <- SF2Prim_Prim2SF. symmetry. rewrite <- SF2Prim_Prim2SF. now rewrite H. Qed.
imports: ZArith Uint63 SpecFloat PrimFloat FloatOps