src/HOL/OrderedGroup.thy

   by (simp add: le_def_join pprt_def join_aci)
 
 lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
   by (simp add: le_def_meet nprt_def meet_aci)
 
+lemma pprt_neg: "pprt (-x) = - nprt x"
+  by (simp add: pprt_def nprt_def)
+
+lemma nprt_neg: "nprt (-x) = - pprt x"
+  by (simp add: pprt_def nprt_def)
+
 lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
 by (simp)
 
 lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
 by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts)

 lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]
 lemmas diff_le_0_iff_le = le_iff_diff_le_0 [symmetric]
 declare diff_less_0_iff_less [simp]
 declare diff_eq_0_iff_eq [simp]
 declare diff_le_0_iff_le [simp]
+
+
 
 
 ML {*
 val add_zero_left = thm"add_0";
 val add_zero_right = thm"add_0_right";