proposition: Lemma hdrel_filter a l : HdRel le a (qs (filter (λ x : A, leb a x) l)).
proof: Proof. apply hd_rel_all. intros. rewrite <- qs_same in H. rewrite filter_In in H. destruct H. pose (refl_le a x). now depelim r. Qed.
imports: Program Utf8 Equations.Prop.Equations Bvector List Relations Arith Wf_nat Lia Coq.Lists.SetoidList Coq.Sorting.Sorting Coq.Sorting.Permutation Coq.Sorting.PermutSetoid Bool EquivDec Permutation