proposition: Lemma all_filterP s : reflect (filter s = s) (all s).
proof: Proof. apply: (iffP idP) => [| <-]; last exact: filter_all. by elim: s => //= x s IHs /andP[-> Hs]; rewrite IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)