proposition: Theorem 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. unfold shl_align_fexp. generalize (shl_align_correct mx ex (fexp (Zpos (digits2_pos mx) + ex))). rewrite Zpos_digits2_pos. case shl_align. intros mx' ex' (H1, H2). split. exact H1. rewrite <- mag_F2R_Zdigits. 2: easy. rewrite <- H1. now rewrite mag_F2R_Zdigits. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative