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