proposition: Theorem shl_align_correct': forall mx ex e, (e <= ex)%Z -> let (mx', ex') := shl_align mx ex e in F2R (Float radix2 (Zpos mx') e) = F2R (Float radix2 (Zpos mx) ex) /\ ex' = e.
proof: Proof. intros mx ex ex' He. unfold shl_align. destruct (ex' - ex)%Z as [|d|d] eqn:Hd ; simpl. - now replace ex with ex' by lia. - exfalso ; lia. - refine (conj _ eq_refl). rewrite shift_pos_correct, Zmult_comm. change (Zpower_pos 2 d) with (Zpower radix2 (Z.opp (Z.neg d))). rewrite <- Hd. replace (- (ex' - ex))%Z with (ex - ex')%Z by ring. now apply eq_sym, F2R_change_exp. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative