proposition: Lemma real_correct : forall f, real f = match toX f with Xnan => false | _ => true end.
proof: Proof. intros. case f ; simpl. apply refl_equal. intros m e. unfold toX. simpl. now case (mantissa_sign m). Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig