(*** le_O_n *)
lemma nle_zero_sx (m): 𝟎 ≤ m.
-#m @(nat_ind … m) -m /2 width=1 by nle_succ_dx/
+#m @(nat_ind_succ … m) -m /2 width=1 by nle_succ_dx/
qed.
(*** le_S_S *)
qed.
(*** le_or_ge *)
-lemma nle_ge_e (m) (n): ∨∨ m ≤ n | n ≤ m.
-#m @(nat_ind … m) -m [ /2 width=1 by or_introl/ ]
-#m #IH #n @(nat_ind … n) -n [ /2 width=1 by or_intror/ ]
-#n #_ elim (IH n) -IH /3 width=2 by nle_succ_bi, or_introl, or_intror/
+lemma nle_ge_dis (m) (n): ∨∨ m ≤ n | n ≤ m.
+#m #n @(nat_ind_succ_2 … m n) -m -n
+[ /2 width=1 by or_introl/
+| /2 width=1 by or_intror/
+| #m #n * /3 width=2 by nle_succ_bi, or_introl, or_intror/
+]
qed-.
(* Basic inversions *********************************************************)
/3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/ qed-.
lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥.
-#m @(nat_ind … m) -m [| #m #IH ] #H
+#m @(nat_ind_succ … m) -m [| #m #IH ] #H
[ /3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/
| /3 width=1 by nle_inv_succ_bi/
]
(* Advanced eliminations ****************************************************)
+(*** le_elim *)
lemma nle_ind_alt (Q: relation2 nat nat):
(∀n. Q (𝟎) (n)) →
(∀m,n. m ≤ n → Q m n → Q (↑m) (↑n)) →
∀m,n. m ≤ n → Q m n.
-#Q #IH1 #IH2 #m #n @(nat_ind_2 … m n) -m -n //
+#Q #IH1 #IH2 #m #n @(nat_ind_succ_2 … m n) -m -n //
[ #m #H elim (nle_inv_succ_zero … H)
| /4 width=1 by nle_inv_succ_bi/
]
(*** decidable_le *)
lemma nle_dec (m) (n): Decidable … (m ≤ n).
-#m #n elim (nle_ge_e m n) [ /2 width=1 by or_introl/ ]
+#m #n elim (nle_ge_dis m n) [ /2 width=1 by or_introl/ ]
#Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ]
/4 width=1 by nle_antisym, or_intror/
qed-.