(* Equalities ***************************************************************)

(*** plus_minus_plus_plus_l *) (**)
lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
#H1 #H2 #H3 #H4
<nplus_assoc <nminus_plus_dx_bi // qed-.

fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
/2 width=1 by plus_minus_minus_be/ qed-.

(* Properties ***************************************************************)

(*** lt_plus_Sn_r *) (**)
lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
/2 width=1/ 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.

(* Inversion & forward lemmas ***********************************************)

lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
#y #z #x elim x -x /3 width=1 by le_S_S_to_le/
#H elim (le_plus_xSy_O_false … H)
qed-.

lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
/2 width=4 by le_plus_xySz_x_false/ qed-.

lemma nat_elim_le_sn (Q:relation …):
      (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
      ∀n1,n2. n1 ≤ n2 → Q n1 n2.
#Q #IH #n1 #n2 #Hn
<(minus_minus_m_m … Hn) -Hn
lapply (minus_le n2 n1)
let d ≝ (n2-n1)
@(nat_elim1 … d) -d -n1 #d
@pull_2 #Hd
<(minus_minus_m_m … Hd) in ⊢ (%→?); -Hd
let n1 ≝ (n2-d) #IHd
@IH -IH [| // ] #m #Hn
/4 width=3 by lt_to_le, lt_to_le_to_lt/
qed-.

(* Decidability of predicates ***********************************************)

lemma dec_lt (R:predicate nat):
      (∀n. Decidable … (R n)) →
      ∀n. Decidable … (∃∃m. m < n & R m).
#R #HR #n elim n -n [| #n * ]
[ @or_intror * /2 width=2 by lt_zero_false/
| * /4 width=3 by lt_S, or_introl, ex2_intro/
| #H0 elim (HR n) -HR
  [ /3 width=3 by or_introl, ex2_intro/
  | #Hn @or_intror * #m #Hmn #Hm
    elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
    /4 width=3 by lt_S_S_to_lt, ex2_intro/
  ]
]
qed-.

lemma dec_min (R:predicate nat):
      (∀n. Decidable … (R n)) → ∀n. R n →
      ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
#R #HR #n
@(nat_elim1 n) -n #n #IH #Hn
elim (dec_lt … HR n) -HR [ -Hn | -IH ]
[ * #p #Hpn #Hp
  elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm
  @(ex3_intro … Hm HNm) -HNm
  /3 width=3 by lt_to_le, le_to_lt_to_lt/
| /4 width=4 by ex3_intro, ex2_intro/
]
qed-.