proposition: Lemma adjust_mantissa_correct : forall mode s m pos, Zpos (adjust_mantissa mode m pos s) = mode_choice mode s (Zpos m) (convert_location_inv pos).
proof: Proof. intros mode s m pos. unfold adjust_mantissa, need_change, mode_choice. case mode ; case s ; case pos ; simpl ; try apply Zpos_succ_morphism ; try apply refl_equal. destruct m ; try apply Zpos_succ_morphism ; try apply refl_equal. destruct m ; try apply Zpos_succ_morphism ; try apply refl_equal. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic