diff --git a/util/counting.v b/util/counting.v
index e087732f89df6cf7d7bc8e97fa3e2daedc45e823..f3ab8e42ffdfda42710da6f0fff45c81ffc310ae 100644
--- a/util/counting.v
+++ b/util/counting.v
@@ -4,6 +4,15 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 (* Additional lemmas about counting. *)
 Section Counting.
   
+  Lemma count_filter_fun :
+    forall (T: eqType) (l: seq T) P,
+      count P l = size (filter P l).
+  Proof.
+    intros T l P.
+    induction l; simpl; first by done.
+    by destruct (P a); [by rewrite add1n /=; f_equal | by rewrite add0n].
+  Qed.
+
   Lemma count_or :
     forall (T: eqType) (l: seq T) P Q,
       count (fun x => P x || Q x) l <= count P l + count Q l. 
diff --git a/util/sorting.v b/util/sorting.v
index 30d2f7d89c6190d9fbd9721d3521de5bda5f7413..ae0bbcecbaa81f8f7cd46d7601e7d3be246aaec4 100644
--- a/util/sorting.v
+++ b/util/sorting.v
@@ -20,6 +20,18 @@ Section Sorting.
     by rewrite addnS ltnS leq_addr.
   Qed.
 
+  Lemma sort_ordered:
+    forall {T: eqType} (leT: rel T) (s: seq T) x0 idx,
+      sorted leT s ->
+      idx < (size s).-1 ->
+      leT (nth x0 s idx) (nth x0 s idx.+1).
+  Proof.
+    intros T leT s x0 idx SORT LT.
+    induction s; first by rewrite /= ltn0 in LT.
+    simpl in SORT, LT; move: SORT => /pathP SORT.
+    by simpl; apply SORT.
+  Qed.
+  
   Lemma sorted_rcons_prefix :
     forall {T: eqType} (leT: rel T) s x,
       sorted leT (rcons s x) ->