Adress PR review (1)

Author: cassiersg

theories/datatypes/List.ec

@@ -3,7 +3,7 @@
 
 
 (* -------------------------------------------------------------------- *)
-require import AllCore StdOrder.
+require import AllCore.
 
 (* -------------------------------------------------------------------- *)
 type 'a list = [
@@ -470,22 +470,25 @@ proof.
   by case (hs = x) => /= _ //; rewrite addrC ltzS count_ge0.
 qed.
 
-lemma count_impl ['a] (p1 p2 : 'a -> bool) (s : 'a list) :
+lemma le_in_count ['a] (p1 p2 : 'a -> bool) (s : 'a list) :
   (forall x, x \in s => p1 x => p2 x) =>
   count p1 s <= count p2 s.
 proof.
-  elim: s => // x s IH h /=.
-  apply IntOrder.ler_add.
-  + by apply /le_b2i /(h x) /in_cons.
-  by apply IH => y hy; apply /(h y) /in_cons; rewrite hy.
+have ler_add: forall (x y z w: int), x <= z => y <= w => x + y <= z + w.
++ move => x y z w h h'.
+  by rewrite (lez_trans (x + w)) 1:lez_add2l 1:h' lez_add2r h.
+elim: s => // x s IH h /=.
+apply ler_add.
++ by apply /le_b2i /(h x) /in_cons.
+by apply IH => y hy; apply /(h y) /in_cons; rewrite hy.
 qed.
 
-lemma count_or ['a] (p1 p2 p : 'a -> bool) (s : 'a list) :
+lemma countU ['a] (p1 p2 p : 'a -> bool) (s : 'a list) :
   (forall x, x \in s => p x => p1 x \/ p2 x) =>
   count p s <= count p1 s + count p2 s.
 proof.
-  elim s => // x s hind h /=.
-  apply (lez_trans ((b2i (p1 x) + b2i (p2 x)) + (count p1 s + count p2 s))) => /#.
+elim s => // x s hind h /=.
+apply (lez_trans ((b2i (p1 x) + b2i (p2 x)) + (count p1 s + count p2 s))) => /#.
 qed.
 
 op has (p : 'a -> bool) xs =