proposition: Lemma all_filter (p q : pred T) xs : all p (filter q xs) = all [pred i | q i ==> p i] xs.
proof: Proof. by elim: xs => //= x xs <-; case: (q x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)