proposition: Theorem snd_shl_align : forall mx ex ex', (ex' <= ex)%Z -> snd (shl_align mx ex ex') = ex'.
proof: Proof. intros mx ex ex' He. generalize (shl_align_correct' mx ex ex' He). now destruct shl_align as [m e]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative