remove [util.counting.v]

lemma [count_filter_fun] is equivalent to ssreflect's [size_filter]

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.

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

classic/util/counting.v

-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.
+End Counting.
\ No newline at end of file

util/all.v

 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.

util/counting.v

-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