proposition: Lemma is_zero_correct_float : forall beta s m e, is_zero (FtoR beta s m e) = false.
proof: Proof. intros beta s m e. rewrite FtoR_split. case is_zero_spec ; try easy. intros H. apply eq_0_F2R in H. now destruct s. Qed.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal