proposition: Lemma adjust_mantissa_correct : forall mode m pos sign, valid_mantissa m -> MtoP (adjust_mantissa mode m pos sign) = Generic.adjust_mantissa mode (MtoP m) pos sign /\ valid_mantissa (adjust_mantissa mode m pos sign).
proof: Proof. intros mode m pos sign Hm. unfold adjust_mantissa, Generic.adjust_mantissa. rewrite mantissa_even_correct with (1 := Hm). unfold Z.even. case need_change. 2: now split. destruct mantissa_one_correct as (Oe, Ov). rewrite Pplus_one_succ_r. rewrite <- Oe. now apply mantissa_add_correct. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig