proposition: Lemma fromZ_correct' : forall n, toX (fromZ n) = Xreal (IZR n).
proof: Proof. intros. unfold toX. simpl. generalize (mantissa_sign_correct (ZtoM n)). case_eq (mantissa_sign (ZtoM n)) ; intros ; rewrite ZtoM_correct in *. rewrite H0. apply refl_equal. rewrite exponent_zero_correct. rewrite (proj1 H0). now case s. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig