proposition: Lemma zero_correct : toX zero = Xreal 0.
proof: Proof. generalize (mantissa_sign_correct mantissa_zero). unfold toX. simpl. case (mantissa_sign mantissa_zero). trivial. rewrite mantissa_zero_correct. intros s p. case s ; intros (H, _) ; discriminate H. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig