proposition: Lemma filter_reverse l : filter P (reverse l) = reverse (filter P l).
proof: Proof. induction l as [|x l IHl]; [done|]. rewrite reverse_cons, filter_app, IHl, !filter_cons. case_decide; [by rewrite reverse_cons|by rewrite filter_nil, app_nil_r]. Qed.
imports: stdpp(options)