---

Step * of Lemma length-filter-lower-bound

∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List]. ∀[T:Type]. ∀[k:ℕ]. ∀[f:{i:ℕ||L||| ¬↑P[L[i]]}  ⟶ T].
  ((||L|| - k) ≤ ||filter(P;L)||) supposing (T ~ ℕk and Inj({i:ℕ||L||| ¬↑P[L[i]]} ;T;f))
BY
{ TACTIC:(Auto THEN Assert ⌜∃a:ℕ. ((a ≤ k) ∧ {i:ℕ||L||| ¬↑P[L[i]]}  ~ ℕa)⌝⋅) }

1
.....assertion..... 
1. A : Type
2. P : A ⟶ 𝔹
3. L : A List
4. T : Type
5. k : ℕ
6. f : {i:ℕ||L||| ¬↑P[L[i]]}  ⟶ T
7. Inj({i:ℕ||L||| ¬↑P[L[i]]} ;T;f)
8. T ~ ℕk
⊢ ∃a:ℕ. ((a ≤ k) ∧ {i:ℕ||L||| ¬↑P[L[i]]}  ~ ℕa)

2
1. A : Type
2. P : A ⟶ 𝔹
3. L : A List
4. T : Type
5. k : ℕ
6. f : {i:ℕ||L||| ¬↑P[L[i]]}  ⟶ T
7. Inj({i:ℕ||L||| ¬↑P[L[i]]} ;T;f)
8. T ~ ℕk
9. ∃a:ℕ. ((a ≤ k) ∧ {i:ℕ||L||| ¬↑P[L[i]]}  ~ ℕa)
⊢ (||L|| - k) ≤ ||filter(P;L)||

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].  \mforall{}[T:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[f:\{i:\mBbbN{}||L|||  \mneg{}\muparrow{}P[L[i]]\}    {}\mrightarrow{}  T].
    ((||L||  -  k)  \mleq{}  ||filter(P;L)||)  supposing  (T  \msim{}  \mBbbN{}k  and  Inj(\{i:\mBbbN{}||L|||  \mneg{}\muparrow{}P[L[i]]\}  ;T;f))


By

---

Latex:
TACTIC:(Auto  THEN  Assert  \mkleeneopen{}\mexists{}a:\mBbbN{}.  ((a  \mleq{}  k)  \mwedge{}  \{i:\mBbbN{}||L|||  \mneg{}\muparrow{}P[L[i]]\}    \msim{}  \mBbbN{}a)\mkleeneclose{}\mcdot{})

---

Home Index