proposition: Lemma FLT_pos_is_pos: forall x, 0 <= x -> 0 <= round_flt x.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. apply round_pred_ge_0 with (Rnd_NE_pt beta (FLT_exp emin prec)) x; auto. apply Rnd_NE_pt_monotone; auto... apply Rnd_NG_pt_refl. apply generic_format_0. apply round_NE_pt... Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)