proposition: Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z).
proof: Proof. intros z; case z; unfold Z.abs. - apply Rabs_R0. - now intros p0; apply Rabs_pos_eq, (IZR_le 0). - unfold IZR at 1. intros p0; rewrite Rabs_Ropp. now apply Rabs_pos_eq, (IZR_le 0). Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp