proposition: Theorem mag_round_ge : forall x, round rnd x <> 0%R -> (mag beta x <= mag beta (round rnd x))%Z.
proof: Proof. Proof with auto with typeclass_instances. intros x. destruct (round_ZR_or_AW rnd x) as [H|H] ; rewrite H ; clear H ; intros Zr. rewrite mag_round_ZR with (1 := Zr). apply Z.le_refl. apply mag_le_abs. contradict Zr. rewrite Zr. apply round_0... rewrite <- round_AW_abs. rewrite round_AW_UP. apply round_UP_pt. apply Rabs_pos. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop