Hello everyone.

What is simple way to prove a theorem below using ssreflect?

```
Inductive isZero : nat -> Prop := IsZero : isZero 0.
Theorem isZero_contra : isZero 1 -> False.
```

I would do the following:

```
by case E: _ /.
```

Probably https://sympa.inria.fr/sympa/arc/ssreflect/2014-10/msg00006.html is helpful for dealing with more complicated cases.

Thank you very much for the example and for the link.

Andrey Klaus has marked this topic as resolved.

Andrey Klaus has marked this topic as unresolved.

Andrey Klaus has marked this topic as resolved.

Last updated: Sep 30 2023 at 06:01 UTC