proposition: Theorem round_AW_abs : forall x, round Zaway (Rabs x) = Rabs (round Zaway 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_AW_opp. apply Rabs_left1. rewrite <- (round_0 Zaway). apply round_le... now apply Rlt_le. apply Rabs_pos_eq. rewrite <- (round_0 Zaway). apply round_le... now apply Rge_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop