proposition: Lemma abs_correct : forall x, toX (abs x) = Xabs (toX x) /\ (valid_ub (abs x) = true).
proof: Proof. intros. split; [|easy]. destruct x as [| m e]. apply refl_equal. unfold toX. simpl. generalize (mantissa_sign_correct m). case_eq (mantissa_sign m). simpl. intros -> _. now rewrite Rabs_R0. intros s p H0 [H1 H2]. generalize (toF_float false p e H2). simpl ; intros ->. now rewrite FtoR_abs. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig