arithmetics for λδ

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_le.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
index 82d285e8ec7bf2bdd310ef18f718ca01192a9781..73c14396423e316aea768fe307e290c4108abb85 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
@@ -15,7 +15,7 @@
 include "ground/insert_eq/insert_eq_0.ma".
 include "ground/arith/nat_succ.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
 
 (*** le *)
 (*** le_ind *)
@@ -75,6 +75,11 @@ lemma nle_inv_zero_dx (m): m ≤ 𝟎 → 𝟎 = m.
 ]
 qed-.
 
+(* Advanced inversions ******************************************************)
+
+lemma nle_inv_succ_zero (m): ↑m ≤ 𝟎 → ⊥.
+/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
 [ /3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/
@@ -82,8 +87,6 @@ lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥.
 ]
 qed-.
 
-(* Order properties *********************************************************)
-
 (*** le_to_le_to_eq *)
 theorem nle_antisym (m) (n): m ≤ n → n ≤ m → m = n.
 #m #n #H elim H -n //
@@ -93,13 +96,25 @@ lapply (IH H) -IH -H #H destruct
 elim (nle_inv_succ_sn_refl … Hn)
 qed-.
 
+(* Advanced eliminations ****************************************************)
+
+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 //
+[ #m #H elim (nle_inv_succ_zero … H)
+| /4 width=1 by nle_inv_succ_bi/
+]
+qed-.
+
+(* Advanced constructions ***************************************************)
+
 (*** transitive_le *)
 theorem nle_trans: Transitive … nle.
 #m #n #H elim H -n /3 width=1 by nle_inv_succ_sn/
 qed-.
 
-(* Advanced constructions ***************************************************)
-
 (*** decidable_le *)
 lemma nle_dec (m) (n): Decidable … (m ≤ n).
 #m #n elim (nle_ge_e m n) [ /2 width=1 by or_introl/ ]