proposition: Theorem abs_round_le_generic : forall x y, generic_format y -> (Rabs x <= y)%R -> (Rabs (round rnd x) <= y)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y. apply round_abs_abs... clear rnd valid_rnd x. intros rnd' Hrnd x Hx. apply round_le_generic... Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop