-lemma nlt_ge_dis (m) (n): ∨∨ m < n | n ≤ m.
-#m #n elim (nle_ge_dis m n) /2 width=1 by or_intror/
-#H elim (nle_lt_eq_dis … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
+lemma nat_split_lt_ge (m) (n): ∨∨ m < n | n ≤ m.
+#m #n elim (nat_split_le_ge m n) /2 width=1 by or_intror/
+#H elim (nle_split_lt_eq … H) -H /2 width=1 by nle_refl, or_introl, or_intror/