strict order relation for natural numbers with inifinity

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_le.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma
index e706fa4dd6c4c933019b39f8bb89b17114b2527c..be13774f5813aa5ca9fcb86b3669f3e3d65f58a8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma
@@ -26,15 +26,21 @@ interpretation "ynat 'less or equal to'" 'leq x y = (yle x y).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact yle_inv_inj_aux: ∀x,y. x ≤ y → ∀m,n. x = yinj m → y = yinj n → m ≤ n.
+fact yle_inv_inj2_aux: ∀x,y. x ≤ y → ∀n. y = yinj n →
+                       ∃∃m. m ≤ n & x = yinj m.
 #x #y * -x -y
-[ #x #y #Hxy #m #n #Hx #Hy destruct //
-| #x #m #n #_ #Hy destruct
+[ #x #y #Hxy #n #Hy destruct /2 width=3 by ex2_intro/
+| #x #n #Hy destruct
 ]
 qed-.
 
+lemma yle_inv_inj2: ∀x,n. x ≤ yinj n → ∃∃m. m ≤ n & x = yinj m.
+/2 width=3 by yle_inv_inj2_aux/ qed-.
+
 lemma yle_inv_inj: ∀m,n. yinj m ≤ yinj n → m ≤ n.
-/2 width=5 by yle_inv_inj_aux/ qed-.
+#m #n #H elim (yle_inv_inj2 … H) -H
+#x #Hxn #H destruct //
+qed-.
 
 fact yle_inv_O2_aux: ∀m:ynat. ∀x:ynat. m ≤ x → x = 0 → m = 0.
 #m #x * -m -x
@@ -63,7 +69,7 @@ fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → ∃∃n. m ≤ n
   #m #Hnm #H destruct
   @(ex2_intro … m) /2 width=1 by yle_inj/ (**) (* explicit constructor *)
 | #x #y #H destruct
-  @(ex2_intro … (∞)) /2 width=1 by yle_Y/
+  @(ex2_intro … (∞)) /2 width=1 by yle_Y/ (**) (* explicit constructor *)
 ]
 qed-.
 
@@ -106,6 +112,6 @@ theorem yle_trans: Transitive … yle.
 [ #x #y #Hxy * //
   #z #H lapply (yle_inv_inj … H) -H
   /3 width=3 by transitive_le, yle_inj/ (**) (* full auto too slow *)
-| #x #z #H lapply ( yle_inv_Y1 … H) //
+| #x #z #H lapply (yle_inv_Y1 … H) //
 ]
 qed-.