proposition: Theorem gt_0_round_gt_0_FLX : forall rnd {Vr: Valid_rnd rnd} x, (0 < x)%R -> (0 < round beta FLX_exp rnd x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros rnd Hr x Hx. assert (K: (0 <= round beta FLX_exp rnd x)%R). rewrite <- (round_0 beta FLX_exp rnd). apply round_le... now apply Rlt_le. destruct K; try easy. absurd (x = 0)%R. now apply Rgt_not_eq. apply eq_0_round_0_FLX with rnd... Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE