Apply suggestions from code review

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>

2 files changed, 2 insertions, 4 deletions

diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 04caf36..350e066 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -227,7 +227,7 @@ Proof. by move=> Pxs; rewrite filter_mask; exact: path_mask_in. Qed.
 Lemma cycle_mask_in m s : all P s -> cycle leT s -> cycle leT (mask m s).
 Proof.
 case: (resize_mask m s) => {m} m sizeE ->.
-elim: m s sizeE => [|[]m ih] [|x s] //= [sizeE] /andP [Px Ps].
+elim: m s sizeE => [|[] m ih] [|x s] //= [sizeE] /andP[Px Ps].
 - rewrite -!cats1 -(mask_cat [:: true] [:: x]) //.
   by apply: path_mask_in; rewrite /= all_cat /= Px Ps.
 - move=> xsx; apply: ih => // {sizeE}; case: s xsx Ps => //= y s.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 57cee21..18e7dac 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1923,9 +1923,7 @@ Lemma mask_cat m1 m2 s1 s2 :
 Proof. by move: m1 s1; apply: seq_ind2 => // -[] m1 x1 s1 /= _ ->. Qed.
 
 Lemma all_mask a m s : all a s -> all a (mask m s).
-Proof.
-by elim: m s => [|[] m IHm] [|x s] //= /andP [? /IHm ->]; rewrite ?andbT.
-Qed.
+Proof. by elim: s m => [|x s IHs] [|[] m]//= /andP[ax /IHs->]; rewrite ?ax. Qed.
 
 Lemma has_mask_cons a b m x s :
   has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).