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