proposition: Lemma before_filter x y l a (l1 := [seq i <- l | a i]) : x \in l1 -> x =[l]< y -> x =[l1]< y.
proof: Proof. rewrite {}/l1 /before; elim: l => //= z l IH. case E : (a z) => /=. rewrite inE eq_sym. by case: eqP => //= Hx; case: eqP. move=> xIl Hi; apply: IH => //. by case: eqP xIl Hi => [<-| _]; [rewrite mem_filter E | case: eqP]. Qed.
imports: mathcomp(all_ssreflect) extra