proposition: Lemma round_FLX_gt_0: forall rnd, Valid_rnd rnd -> Prec_gt_0 prec -> forall x, 0 < x -> 0 < round beta (FLX_exp prec) rnd x.
proof: Proof. Proof with auto with typeclass_instances. intros rnd Hrnd Hprec x Hx. destruct (mag beta x) as (e,He). apply Rlt_le_trans with (round beta (FLX_exp prec) rnd (bpow (e-1))). rewrite round_generic... apply bpow_gt_0. apply generic_format_bpow. unfold FLX_exp; unfold Prec_gt_0 in Hprec; lia. apply round_le... rewrite <- Rabs_right. apply He, Rgt_not_eq; easy. apply Rle_ge; left; easy. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic) ComputeMore Flocq(Bracket Round Operations Div)