diff --git a/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
index e652e58b7461d942c2cb9c3acd088b69008417c9..196493031cae83ece9324cd70c97e54ab37b7241 100644
--- a/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -585,7 +585,7 @@ Section Sequential_Abstract_RTA.
         { by move: ARR => [t ARR]; rewrite subnKC //; feed (H_arrival_times_are_consistent j t); try (subst t). }
         have Fact1: 1 <= number_of_task_arrivals arr_seq tsk (t1 + A) (t1 + A + ε).
         { rewrite /number_of_task_arrivals /task_arrivals_between /arrival_sequence.arrivals_between.
-          by rewrite -count_filter_fun -has_count; apply/hasP; exists j; last rewrite TSK.
+          by rewrite size_filter -has_count; apply/hasP; exists j; last rewrite TSK.
         }
         rewrite (@num_arrivals_of_task_cat _ _ _ _ _ (t1 + A)); last by apply/andP; split; rewrite leq_addr //.
         rewrite mulnDr.
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v b/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
index 12041b4620a04acc58f370fa84f75b47cb799f3a..d0bd64b51617fafadd5f28d69b53d9c0c3200d0f 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
@@ -494,7 +494,7 @@ Module AbstractSeqRTA.
             } 
             have Fact1: num_arrivals_of_task job_task arr_seq tsk (t1 + A) (t1 + A + ε) >= 1.
             { rewrite /num_arrivals_of_task /arrivals_of_task_between.
-              rewrite -count_filter_fun -has_count; apply/hasP.
+              rewrite size_filter -has_count; apply/hasP.
                 by exists j; last rewrite /is_job_of_task TSK.
             }
             have Fact2: job_cost j <= task_workload_between (t1 + A) (t1 + A + ε).
@@ -636,4 +636,4 @@ Module AbstractSeqRTA.
   End Sequential_Abstract_RTA. 
   
 End AbstractSeqRTA.
- 
\ No newline at end of file
+ 
diff --git a/classic/util/counting.v b/classic/util/counting.v
index d4e23a53dc1fb87767f8461b8a8ac805f840e473..03f4b6251ad79c2f542ea8e565edca63f8600c21 100644
--- a/classic/util/counting.v
+++ b/classic/util/counting.v
@@ -1,5 +1,3 @@
-Require Export prosa.util.counting.
-
 Require Import prosa.classic.util.tactics prosa.classic.util.ord_quantifier.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
@@ -103,4 +101,4 @@ Section Counting.
     }
   Qed.
 
-End Counting.
\ No newline at end of file
+End Counting.
diff --git a/util/all.v b/util/all.v
index cdc1a9d9584aa3de411b6cab24fd0774ca70a21b..20dc35795980047b49c4750db5ff56e42e0d4a10 100644
--- a/util/all.v
+++ b/util/all.v
@@ -1,7 +1,6 @@
 Require Export prosa.util.tactics.
 Require Export prosa.util.notation.
 Require Export prosa.util.bigcat.
-Require Export prosa.util.counting.
 Require Export prosa.util.div_mod.
 Require Export prosa.util.list.
 Require Export prosa.util.nat.
diff --git a/util/counting.v b/util/counting.v
deleted file mode 100644
index 0fec37401fb94b4dd2a8814822318323b7f1a5ee..0000000000000000000000000000000000000000
--- a/util/counting.v
+++ /dev/null
@@ -1,15 +0,0 @@
-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.
-
-End Counting.
\ No newline at end of file