-lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
-/2 width=4 by plus_xySz_x_false/ qed-.
-
-lemma pred_inv_fix_sn: ∀x. ↓x = x → 0 = x.
-* // #x <pred_Sn #H
-elim (succ_inv_refl_sn x) //
-qed-.
-
-lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
-// qed-.
-
-lemma discr_plus_x_xy: ∀x,y. x = x + y → y = 0.
-/2 width=2 by le_plus_minus_comm/ qed-.
-
-lemma plus2_le_sn_sn: ∀m1,m2,n1,n2. m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
-#m1 #m2 #n1 #n2 #H #Hm
-lapply (monotonic_le_plus_l n1 … Hm) -Hm >H -H
-/2 width=2 by le_plus_to_le/
-qed-.
-
-lemma plus2_le_sn_dx: ∀m1,m2,n1,n2. m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
-/2 width=4 by plus2_le_sn_sn/ qed-.
-
-lemma plus2_le_dx_sn: ∀m1,m2,n1,n2. n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
-/2 width=4 by plus2_le_sn_sn/ qed-.
-
-lemma plus2_le_dx_dx: ∀m1,m2,n1,n2. n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
-/2 width=4 by plus2_le_sn_sn/ qed-.
-
-lemma lt_S_S_to_lt: ∀x,y. ↑x < ↑y → x < y.
-/2 width=1 by le_S_S_to_le/ qed-.
-
-(* Note this should go in nat.ma *)
-lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
-#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/
-#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/
-#y #_ >minus_plus_plus_l
-#H lapply (discr_plus_xy_minus_xz … H) -H
-#H destruct
-qed-.
-
-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 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-.
-