+lemma lt_inv_O1: ∀n. 0 < n → ∃m. ↑m = n.
+* /2 width=2 by ex_intro/
+#H cases (lt_le_false … H) -H //
+qed-.
+
+lemma lt_inv_S1: ∀m,n. ↑m < n → ∃∃p. m < p & ↑p = n.
+#m * /3 width=3 by lt_S_S_to_lt, ex2_intro/
+#H cases (lt_le_false … H) -H //
+qed-.
+
+lemma lt_inv_gen: ∀y,x. x < y → ∃∃z. x ≤ z & ↑z = y.
+* /3 width=3 by le_S_S_to_le, ex2_intro/
+#x #H elim (lt_le_false … H) -H //
+qed-.
+
+lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
+/2 width=1 by plus_le_0/ qed-.
+
+lemma plus_inv_S3_sn: ∀x1,x2,x3. x1+x2 = ↑x3 →
+ ∨∨ ∧∧ x1 = 0 & x2 = ↑x3
+ | ∃∃y1. x1 = ↑y1 & y1 + x2 = x3.
+* /3 width=1 by or_introl, conj/
+#x1 #x2 #x3 <plus_S1 #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma plus_inv_S3_dx: ∀x2,x1,x3. x1+x2 = ↑x3 →
+ ∨∨ ∧∧ x2 = 0 & x1 = ↑x3
+ | ∃∃y2. x2 = ↑y2 & x1 + y2 = x3.
+* /3 width=1 by or_introl, conj/
+#x2 #x1 #x3 <plus_n_Sm #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma max_inv_O3: ∀x,y. (x ∨ y) = 0 → 0 = x ∧ 0 = y.
+/4 width=2 by le_maxr, le_maxl, le_n_O_to_eq, conj/
+qed-.
+
+lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
+* /2 width=1 by conj/ #x #y normalize #H destruct
+qed-.
+
+lemma nat_split: ∀x. x = 0 ∨ ∃y. ↑y = x.
+* /3 width=2 by ex_intro, or_introl, or_intror/
+qed-.
+
+lemma lt_elim: ∀R:relation nat.
+ (∀n2. R O (↑n2)) →
+ (∀n1,n2. R n1 n2 → R (↑n1) (↑n2)) →
+ ∀n2,n1. n1 < n2 → R n1 n2.
+#R #IH1 #IH2 #n2 elim n2 -n2
+[ #n1 #H elim (lt_le_false … H) -H //
+| #n2 #IH * /4 width=1 by lt_S_S_to_lt/
+]
+qed-.
+
+lemma le_elim: ∀R:relation nat.
+ (∀n2. R O (n2)) →
+ (∀n1,n2. R n1 n2 → R (↑n1) (↑n2)) →
+ ∀n1,n2. n1 ≤ n2 → R n1 n2.
+#R #IH1 #IH2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2
+/4 width=1 by monotonic_pred/ -IH1 -IH2
+#n1 #H elim (lt_le_false … H) -H //
+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-.
+