proposition: Theorem round_neq_0_negligible_exp : negligible_exp = None -> forall rnd { Zrnd : Valid_rnd rnd } x, (x <> 0)%R -> (round beta fexp rnd x <> 0)%R.
proof: Proof. Proof with auto with typeclass_instances. intros H rndn Hrnd x Hx K. case negligible_exp_spec'. intros (_,Hn). destruct (mag beta x) as (e,He). absurd (fexp e < e)%Z. apply Zle_not_lt. apply exp_small_round_0 with beta rndn x... apply (Hn e). intros (n,(H1,_)). rewrite H in H1; discriminate. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop