lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
/2 by plus_minus/ qed.
+lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x.
+// qed.
+
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.
#a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/
qed.
+lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
+/2 width=1 by plus_minus/ qed-.
+
+(* Properties ***************************************************************)
+
+fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+// qed-.
+
+lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
+/3 width=1 by monotonic_le_minus_l/ qed.
+
+(* Note: this might interfere with nat.ma *)
+lemma monotonic_lt_pred: ∀m,n. m < n → O < m → pred m < pred n.
+#m #n #Hmn #Hm whd >(S_pred … Hm)
+@le_S_S_to_le >S_pred /2 width=3 by transitive_lt/
+qed.
+
+lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
+/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
+
+lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1.
+#z #x #y #n #Hzx #Hxny
+>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
+>plus_minus [2: /2 width=1 by lt_to_le/ ]
+/2 width=1 by monotonic_le_minus_l2/
+qed.
+
+lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n.
+#z #x #y #n #Hzx #Hyxn
+>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
+>plus_minus [2: /2 width=1 by lt_to_le/ ]
+/2 width=1 by monotonic_le_minus_l2/
+qed.
+
(* Inversion & forward lemmas ***********************************************)
axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
#Hxy elim (H Hxy)
qed-.
+lemma pred_inv_refl: ∀m. pred m = m → m = 0.
+* // normalize #m #H elim (lt_refl_false m) //
+qed-.
+
lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
#y #z #x elim x -x
[ #H lapply (le_n_O_to_eq … H) -H
#B #f #b #l elim l -l normalize //
qed.
+lemma iter_plus: ∀B:Type[0]. ∀f:B→B. ∀b,l1,l2. f^(l1+l2) b = f^l1 (f^l2 b).
+#B #f #b #l1 elim l1 -l1 normalize //
+qed.
+
(* Trichotomy operator ******************************************************)
(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)