Hello, I've been learning about math-comp and wanted to implement issue 619 a as a challenge. My code is the following

```
Lemma subset_cons2 s1 s2 x:
s1 \subset s2 -> x::s1 \subset x::s2.
Proof.
move/subsetP=> ss1s2; apply/subsetP => y H; rewrite in_cons in H; rewrite in_cons.
apply/orP; case/orP: H.
- by move => p; left; apply p.
- by move => p; right; apply: ss1s2.
Qed.
```

However there are many things that could be improved. I thought that I could apply `in_cons`

directly in `H`

in the 4th line, by `apply/subsetP => y /in_cons-H`

but it's not working. There is also some repetition as I'm using twice the same lemma, both with `in_cons`

and `orP`

.

I'd appreciate any constructive criticism to improve this code.

```
Lemma subset_cons2 s1 s2 (x : T) :
s1 \subset s2 -> x :: s1 \subset x :: s2.
Proof.
move/subsetP=> ss1s2; apply/subsetP => y.
rewrite !inE.
case: eqP => //= _.
apply: ss1s2.
Qed.
```

Thank you!

Last updated: Jul 15 2024 at 21:02 UTC