proposition: Theorem round_le : forall x y, (x <= y)%R -> (round rnd x <= round rnd y)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y Hxy. destruct (total_order_T x 0) as [[Hx|Hx]|Hx]. 3: now apply round_le_pos. unfold round. destruct (Rlt_or_le y 0) as [Hy|Hy]. rewrite <- (Ropp_involutive x), <- (Ropp_involutive y). rewrite (scaled_mantissa_opp (-x)), (scaled_mantissa_opp (-y)). rewrite (cexp_opp (-x)), (cexp_opp (-y)). apply Ropp_le_cancel. rewrite <- 2!F2R_Zopp. apply (round_le_pos (Zrnd_opp rnd) (-y) (-x)). rewrite <- Ropp_0. now apply Ropp_lt_contravar. now apply Ropp_le_contravar. apply Rle_trans with 0%R. apply F2R_le_0. simpl. rewrite <- (Zrnd_IZR rnd 0). apply Zrnd_le... simpl. rewrite <- (Rmult_0_l (bpow (- fexp (mag beta x)))). apply Rmult_le_compat_r. apply bpow_ge_0. now apply Rlt_le. apply F2R_ge_0. simpl. rewrite <- (Zrnd_IZR rnd 0). apply Zrnd_le... apply Rmult_le_pos. exact Hy. apply bpow_ge_0. rewrite Hx. rewrite round_0... apply F2R_ge_0. simpl. rewrite <- (Zrnd_IZR rnd 0). apply Zrnd_le... apply Rmult_le_pos. now rewrite <- Hx. apply bpow_ge_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop