proposition: Theorem round_abs_abs : forall P : R -> R -> Prop, ( forall rnd (Hr : Valid_rnd rnd) x, (0 <= x)%R -> P x (round rnd x) ) -> forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).
proof: Proof. Proof with auto with typeclass_instances. intros P HP rnd Hr x. destruct (Rle_or_lt 0 x) as [Hx|Hx]. rewrite 2!Rabs_pos_eq. now apply HP. rewrite <- (round_0 rnd). now apply round_le. exact Hx. rewrite (Rabs_left _ Hx). rewrite Rabs_left1. pattern x at 2 ; rewrite <- Ropp_involutive. rewrite round_opp. rewrite Ropp_involutive. apply HP... rewrite <- Ropp_0. apply Ropp_le_contravar. now apply Rlt_le. rewrite <- (round_0 rnd). apply round_le... now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop