proposition: Theorem round_ZR_abs : forall x, round Ztrunc (Rabs x) = Rabs (round Ztrunc x).
proof: Proof. Proof with auto with typeclass_instances. intros x. apply sym_eq. unfold Rabs at 2. destruct (Rcase_abs x) as [Hx|Hx]. rewrite round_ZR_opp. apply Rabs_left1. rewrite <- (round_0 Ztrunc). apply round_le... now apply Rlt_le. apply Rabs_pos_eq. rewrite <- (round_0 Ztrunc). apply round_le... now apply Rge_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop