proposition: Theorem Rnd_odd_pt_monotone : round_pred_monotone (Rnd_odd_pt).
proof: Proof. Proof with auto with typeclass_instances. intros x y f g H1 H2 Hxy. apply Rle_trans with (round beta fexp Zrnd_odd x). right; apply Rnd_odd_pt_unique with x; try assumption. apply round_odd_pt. apply Rle_trans with (round beta fexp Zrnd_odd y). apply round_le... right; apply Rnd_odd_pt_unique with y; try assumption. apply round_odd_pt. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations