diff options
| author | Kazuhiko Sakaguchi | 2020-11-05 21:45:23 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-11 00:46:15 +0900 |
| commit | c312c678ac8af99d5c632285cbff5e1b55325478 (patch) | |
| tree | 526e0fb9dc2c91b1cbf118aa222eec5893e79156 /mathcomp/ssreflect/seq.v | |
| parent | 126a1b7be3ab3ef3cb16887bc31d0011fb4b88d4 (diff) | |
Apply suggestions from code review
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 4 |
1 files changed, 1 insertions, 3 deletions
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). |