proposition: Lemma filter_incl_surj (T : eqType) (x : T) (l : seq T) (P : pred T) : let l' := [seq x <- l | P x] in forall (f : 'I_(size l') -> 'I_(size l)), (forall i : 'I_(size l'), nth x l (f i) = nth x l' i) -> {homo f : x0 y / x0 < y >-> x0 < y} -> forall j : 'I_(size l), P (nth x l j) -> exists i : 'I_(size l'), j = f i.
proof: Proof. set l' := [seq x0 <- l | P x0]=>/= f fi fh j Pj. suff: exists i, ~~ (j != f i) by move=>[i /negPn/eqP ->]; exists i. apply /existsP. rewrite -negb_forall; apply /negP=>/forallP jf. suff: size l' < count P l by rewrite size_filter lt_irreflexive. rewrite (count_card x). have what: (size l' < (size l').+1) by move:(leqnn (size l').+1). apply (lt_le_trans what). rewrite -(card_ord (size l').+1). have/card_codom<-: injective (fun i => match ord_S_split i with | inleft j => f (proj1_sig j) | _ => j end). move=>a b. case:(ord_S_split a). move=>[a'/= ae]; subst a. case:(ord_S_split b). move=>[b'/= be]; subst b=>fab. apply val_inj; apply/eqP; rewrite/=/bump/= 2!add1n eqSS. by apply/negP=>/negP/lt_total/orP; case=>/fh; rewrite fab lt_irreflexive. by move=>->/esym je; move:(jf a'); rewrite je eq_refl. case:(ord_S_split b). by move=>[b'/= be]; subst b=>fab je; move:(jf b'); rewrite je eq_refl. by move=>-> -> _. apply subset_leq_card; apply/subsetP=>k /codomP [a ->]. case: (ord_S_split a). move=>[a'/= _]; rewrite inE fi. have/mem_nth: val a' < size l' by case: a'. by move=>/(_ x); rewrite mem_filter=>/andP[h _]. by move=>_; rewrite inE. Qed.
imports: mathcomp(all_ssreflect ssrnum zmodp order constructive_ereal) preliminaries