proposition: Lemma round_le_pos : forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R.
proof: Proof. intros x y Hx Hxy. destruct (mag beta x) as [ex Hex]. destruct (mag beta y) as [ey Hey]. specialize (Hex (Rgt_not_eq _ _ Hx)). specialize (Hey (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ Hx Hxy))). rewrite Rabs_pos_eq in Hex. 2: now apply Rlt_le. rewrite Rabs_pos_eq in Hey. 2: apply Rle_trans with (2:=Hxy); now apply Rlt_le. assert (He: (ex <= ey)%Z). apply bpow_lt_bpow with beta. apply Rle_lt_trans with (1 := proj1 Hex). now apply Rle_lt_trans with y. assert (Heq: fexp ex = fexp ey -> (round x <= round y)%R). intros H. unfold round, scaled_mantissa, cexp. rewrite mag_unique_pos with (1 := Hex). rewrite mag_unique_pos with (1 := Hey). rewrite H. apply F2R_le. apply Zrnd_le. apply Rmult_le_compat_r with (2 := Hxy). apply bpow_ge_0. destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1]. apply Heq. apply valid_exp with (1 := Hy1). now apply Z.le_trans with ey. destruct (Zle_lt_or_eq _ _ He) as [He'|He']. 2: now apply Heq, f_equal. apply Rle_trans with (bpow (ey - 1)). 2: now apply round_bounded_large_pos. destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1]. destruct (round_bounded_small_pos _ _ Hx1 Hex) as [-> | ->]. apply bpow_ge_0. apply bpow_le. apply valid_exp, proj2 in Hx1. specialize (Hx1 ey). lia. apply Rle_trans with (bpow ex). now apply round_bounded_large_pos. apply bpow_le. now apply Z.lt_le_pred. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop