proposition: Theorem round_le_generic : forall x y, generic_format y -> (x <= y)%R -> (round rnd x <= y)%R.
proof: Proof. intros x y Hy Hxy. rewrite <- (round_generic rnd y Hy). now apply round_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop