proposition: Theorem round_DN_pt : forall x, Rnd_DN_pt generic_format x (round Zfloor x).
proof: Proof. Proof with auto with typeclass_instances. intros x. split. apply generic_format_round... split. pattern x at 2 ; rewrite <- scaled_mantissa_mult_bpow. unfold round, F2R. simpl. apply Rmult_le_compat_r. apply bpow_ge_0. apply Zfloor_lb. intros g Hg Hgx. apply round_ge_generic... Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop