proposition: Theorem round_generic : forall x, generic_format x -> round x = x.
proof: Proof. intros x Hx. unfold round. rewrite scaled_mantissa_generic with (1 := Hx). rewrite Zrnd_IZR. now apply sym_eq. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop