proposition: Theorem shl_align_correct : forall mx ex ex', let (mx', ex'') := shl_align mx ex ex' in F2R (Float radix2 (Zpos mx) ex) = F2R (Float radix2 (Zpos mx') ex'') /\ (ex'' <= ex')%Z.
proof: Proof. intros mx ex ex'. generalize (shl_align_correct' mx ex ex'). unfold shl_align. destruct (ex' - ex)%Z as [|d|d] eqn:Hd ; simpl. - refine (fun H => _ (H _)). 2: clear -Hd; lia. clear. intros [H1 ->]. now split. - intros _. refine (conj eq_refl _). lia. - refine (fun H => _ (H _)). 2: clear -Hd; lia. clear. now split. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative