proposition: Lemma Prim2SF2R_Prim2B2R : forall x, SF2R radix2 (Prim2SF x) = B2R (Prim2B x).
proof: Proof. intros x. now rewrite <-SF2R_B2SF, B2SF_Prim2B. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)