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