proposition: Lemma shl_align_fexp_correct : forall mx ex, let (mx', ex') := shl_align_fexp mx ex in F2R (Float radix2 (Zpos mx) ex) = F2R (Float radix2 (Zpos mx') ex') /\ (ex' <= fexp (Zdigits radix2 (Zpos mx') + ex'))%Z.
proof: Proof. intros mx ex. apply shl_align_fexp_correct. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN