+axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+
+axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
+
+lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
+#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/
+#H elim H -m /2 width=1 by or3_intro1/
+#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/
+qed-.
+