+lemma lt_refl_false: ∀n. n < n → False.
+#n #H elim (lt_to_not_eq … H) -H /2/
+qed.
+
+lemma lt_zero_false: ∀n. n < 0 → False.
+#n #H elim (lt_to_not_le … H) -H /2/
+qed.
+
+lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
+#m #n elim (decidable_lt m n) /3/
+qed.
+
+lemma plus_lt_false: ∀m,n. m + n < m → False.
+#m #n #H1 lapply (le_plus_n_r n m) #H2
+lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
+elim (lt_refl_false … H)
+qed.
+
+lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
+#n #m <plus_n_Sm #H destruct
+qed.
+
+lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
+/3/ qed.
+