proposition: Theorem generic_format_EM : forall x, generic_format x \/ ~generic_format x.
proof: Proof. Proof with auto with typeclass_instances. intros x. destruct (Req_dec (round Zfloor x) x) as [Hx|Hx]. left. rewrite <- Hx. apply generic_format_round... right. intros H. apply Hx. apply round_generic... Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop