(* 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
#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-.
[ #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-.