Apply suggestions from Kazuhiko

Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>

1 files changed, 21 insertions, 22 deletions

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 14a7c26..9747171 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1271,13 +1271,17 @@ elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}].
 by rewrite in_cons; case: (eqVneq y x) => // <-; rewrite s'y.
 Qed.
 
-Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} ->
-  (forall x, count_mem x s1 <= count_mem x s2).
+Lemma leq_uniq_countP x s1 s2 : uniq s1 ->
+  reflect (x \in s1 -> x \in s2) (count_mem x s1 <= count_mem x s2).
 Proof.
-move=> s1_uniq s1_s2 x; rewrite count_uniq_mem//.
-by case: (boolP (_ \in _)) => // /s1_s2/count_memPn/eqP; rewrite -lt0n.
+move/count_uniq_mem->; case: (boolP (_ \in _)) => //= _; last by constructor.
+by rewrite -has_pred1 has_count; apply: (iffP idP) => //; apply.
 Qed.
 
+Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} ->
+  (forall x, count_mem x s1 <= count_mem x s2).
+Proof. by move=> s1_uniq s1_s2 x; apply/leq_uniq_countP/s1_s2. Qed.
+
 Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x].
 Proof.
 move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)).
@@ -1464,7 +1468,7 @@ Implicit Types x y z : T.
 
 Lemma rot_index s x (i := index x s) : x \in s ->
   rot i s = x :: (drop i.+1 s ++ take i s).
-Proof. by move=> x_s; rewrite /rot drop_index ?cat_cons. Qed.
+Proof. by move=> x_s; rewrite /rot drop_index. Qed.
 
 Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
 
@@ -2218,9 +2222,7 @@ Lemma remE s : rem s = take (index x s) s ++ drop (index x s).+1 s.
 Proof. by elim: s => //= y s ->; case: eqVneq; rewrite ?drop0. Qed.
 
 Lemma rem_id s : x \notin s -> rem s = s.
-Proof.
-by move=> xNs; rewrite remE memNindex ?take_size ?drop_oversize ?cats0.
-Qed.
+Proof. by elim: s => //= y s IHs /norP[neq_yx /IHs->]; case: eqVneq neq_yx. Qed.
 
 Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s).
 Proof.
@@ -2257,15 +2259,14 @@ Proof. by move/mem_rem_uniq->; rewrite inE eqxx. Qed.
 
 Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x.
 Proof.
-have [xs|xNs]/= := boolP (x \in s); last by rewrite subn0 rem_id.
-rewrite -[s in RHS](cat_take_drop (index x s)) drop_index// remE !count_cat/=.
-by rewrite addnCA addKn.
+have [/perm_to_rem/permP->|xNs]/= := boolP (x \in s); first by rewrite addKn.
+by rewrite subn0 rem_id.
 Qed.
 
 Lemma count_mem_rem y s : count_mem y (rem s) = count_mem y s - (x == y).
 Proof.
-rewrite count_rem/=; have [->|] := eqVneq y x; last by rewrite andbF subn0.
-by have [|/count_memPn->] := boolP (x \in _).
+rewrite count_rem; have []//= := boolP (x \in s).
+by case: eqP => // <- /count_memPn->.
 Qed.
 
 End Rem.
@@ -2375,6 +2376,12 @@ Proof. by elim: s => //= x s <-; case: (a x). Qed.
 
 Section MiscMask.
 
+Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s.
+Proof.
+by elim: s m => [|x s IHs] [|[] m]//=;
+   rewrite ?leq_add2l (leq_trans (IHs _)) ?leq_addl.
+Qed.
+
 Variable (T : eqType).
 Implicit Types (s : seq T) (m : bitseq).
 
@@ -2387,12 +2394,6 @@ elim: m s => [|[] m ih] [|x s] //=.
 - by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih].
 Qed.
 
-Lemma leq_count_mask P m s : count P (mask m s) <= count P s.
-Proof.
-by elim: s m => [|x s IHs] [|[] m]//=;
-   rewrite ?leq_add2l (leq_trans (IHs _)) ?leq_addl.
-Qed.
-
 Lemma leq_count_subseq P s1 s2 : subseq s1 s2 -> count P s1 <= count P s2.
 Proof. by move=> /subseqP[m _ ->]; rewrite leq_count_mask. Qed.
 
@@ -2400,9 +2401,7 @@ Lemma count_maskP s1 s2 :
   (forall x, count_mem x s1 <= count_mem x s2) <->
     exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2).
 Proof.
-split=> [s1_le|[m _ /allP/(_ _ _)/eqP s1ms2 x]]; last first.
-  have [xs1|/count_memPn->//] := boolP (x \in s1).
-  by rewrite s1ms2 ?mem_cat ?xs1// leq_count_mask.
+split=> [s1_le|[m _ /permP s1ms2 x]]; last by rewrite s1ms2 leq_count_mask.
 suff [m mP]: exists m, perm_eq s1 (mask m s2).
   by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm.
 elim: s2 => [|x s2 IHs]//= in s1 s1_le *.