-lemma not_included_ex: ∀s1,s2. not_O s2 s1 → ∀i. C s2 i →
- ∃b.〈i, 〈i,b〉〉 ↓ s1 (|〈i,b〉|).
-#s1 #s2 #H #i * #c * #x0 #H1
-cases (H c (max (S(|i|)) x0)) #x1 * #H2 #H3 cases (pad i x1 ?)
- [#b #H4 %{b}
- cases (H1 〈i,b〉 ?)
- [#z >H4 #H5 %{z} @(monotonic_U … H5) @lt_to_le //
- |>H4 @(le_maxr … H2)
- ]
- |@(le_maxl … H2)
+(* a few lemma to prove injective_to_exists. This is a general result; a nice
+example of the pidgeon hole pricniple *)
+
+lemma f_img_to_exists:
+ ∀f.∀n,a. a ∈ f_img f n → ∃b. b < n ∧ f b = a.
+#f #n #a elim n normalize [@False_ind]
+#m #Hind *
+ [#Ha %{m} /2/ |#H cases(Hind H) #b * #Hb #Ha %{b} % // @le_S //]
+qed.
+
+lemma length_f_img: ∀f,n. |f_img f n| = n.
+#f #n elim n // normalize //
+qed.
+
+lemma unique_f_img: ∀f,n. injective … f → unique ? (f_img f n).
+#f #n #Hinj elim n normalize //
+#m #Hind % // % #H lapply(f_img_to_exists …H) * #b * #ltbm
+#eqbm @(absurd … ltbm) @le_to_not_lt >(Hinj… eqbm) //
+qed.
+
+lemma injective_to_exists: ∀f. injective nat nat f →
+ ∀n.(∀i.i < n → f i < n) → ∀a. a < n → ∃b. b<n ∧ f b = a.
+#f #finj #n #H1 #a #ltan @(f_img_to_exists f n a)
+@(eq_length_to_mem_all … (length_f_img …) (unique_f_img …finj …) …ltan)
+#x #Hx cases(f_img_to_exists … Hx) #b * #ltbn #eqx <eqx @H1 //
+qed.
+
+lemma weak_pad1 :∀n,a.∃b. n ≤ 〈a,b〉.
+#n #a
+cut (∀i.decidable (〈a,i〉 < n))
+ [#i @decidable_le ]
+ #Hdec cases(decidable_forall (λb. 〈a,b〉 < n) Hdec n)
+ [#H cut (∀i. i < n → ∃b. b < n ∧ 〈a,b〉 = i)
+ [@(injective_to_exists … H) //]
+ #Hcut %{n} @not_lt_to_le % #Han
+ lapply(Hcut ? Han) * #x * #Hx #Hx2
+ cut (x = n) [//] #Hxn >Hxn in Hx; /2 by absurd/
+ |#H lapply(not_forall_to_exists … Hdec H)
+ * #b * #H1 #H2 %{b} @not_lt_to_le @H2