-lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
-qed-.
-
-lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
-#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/
-qed-.
-
-lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
-/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
-
-lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
- a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
-#a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/
-qed-.
-
-lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
-/2 width=1 by plus_minus/ qed-.
-
-lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 →
- m1+n2 = m2+n1 → m1-n1 = m2-n2.
-/2 width=1 by arith_b1/ qed-.
-