proposition: Lemma filter_succ (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 (i' : 'I_(size l')) k, (f i' < k < (f i'.+1mod + (i'.+1 == size l')*(size l))%N)%N -> ~~ P (nth x l (k %% size l)).
proof: Proof. set l' := [seq x0 <- l | P x0]=>/= f fi fh i' k ikj; apply /negP=>Pkl. have kl: k %% size l < size l. apply ltn_pmod; destruct l=>//. by move:(i')=>[a/= alt]. move: (@filter_incl_surj _ _ _ _ _ fi fh (Ordinal kl) Pkl)=>[[a alt] /(congr1 val)/= ke]. destruct i' as [i' i'lt]. move:(i'lt); rewrite leq_eqVlt => /predU1P[ie|]. move:ikj; rewrite ie eq_refl mul1n. case klt: (k < size l). move:(alt); rewrite -{1}ie leq_eqVlt=>/orP; case. rewrite eqSS=>/eqP ae; subst a. move: ke; rewrite modn_small ?klt//; move=>->/andP. have->:Ordinal alt = Ordinal i'lt by apply val_inj. move=>[h _]. by move: (lt_irreflexive (f (Ordinal i'lt)))=>/negbT/negP; apply. rewrite ltnS=>ai' /andP[fik _]. have/fh fai:Ordinal alt < Ordinal i'lt by []. move:(ltn_trans fai fik); rewrite/= -ke modn_small ?klt//. by rewrite ltnn. move:klt; rewrite ltNge=>/negbT/negbNE lk. move=>/andP[_]; rewrite addnC -ltn_subLR// =>kf. have kmod: (k %% size l = k - size l)%N. rewrite -{1}[k](subnK lk) modnDr modn_small//. by apply (ltn_trans kf). move:ke; rewrite kmod=>ke. have ie' : val (Ordinal i'lt).+1mod = 0%N. by move: ie i'lt {kf}=><- i'lt/=; apply modnn. destruct a as [| a]. have ae: Zp_succ (Ordinal i'lt) = Ordinal alt by apply val_inj. by move: kf; rewrite ke -ae ltnn. have /fh fia : (Ordinal i'lt).+1mod < Ordinal alt. suff: val (Ordinal i'lt).+1mod < a.+1 by []. by rewrite ie'; apply ltn0Sn. have fai: f (Ordinal alt) < f (Ordinal i'lt).+1mod. by have: val (f (Ordinal alt)) < val (f (Ordinal i'lt).+1mod) by rewrite/= -ke. by move:(lt_trans fai fia); rewrite ltxx. move=>i'lt'; move:ikj. case ile: ((Ordinal i'lt).+1 == size l'). by move:ile=>/=/eqP ile; move:i'lt'; rewrite ile ltnn. rewrite/=/muln/muln_rec/= addnC/addn/addn_rec/= => /andP[fk kf]. have kl': (k < size l)%N by apply (ltn_trans kf). move:Pkl kl ke; rewrite modn_small// =>Pkl kl ke. move:fk kf; rewrite ke=>/(@homo_lt_total _ _ _ _ _ fh) ia /(@homo_lt_total _ _ _ _ _ fh) ai. have ia': (i' < a)%N by []. have ai': (a < i'.+1)%N. have ai': val (Ordinal alt) < val (Ordinal i'lt).+1mod by []. move:f fi fh alt i'lt ile {ia} ke i'lt' ai ai'; rewrite/Zp_succ -/l'; generalize (size l'); case=>// n _ _ _ /= _ _ _ _ i'lt _. by rewrite modn_small. by move: (leq_ltn_trans ia' ai'); rewrite ltnn. Qed.
imports: mathcomp(all_ssreflect ssrnum zmodp order constructive_ereal) preliminaries