# A manual proof of discrimination

Prove manually (*i.e* without `Discriminate`)
the inequality `true<>false`.
## Solution

This file
### Note

The definition of the local function `is_true` is a beautiful
illustration of the relationship between `bool` and `Prop`.

Notice the use of `change`, which illustrates the importance
of type conversion.

Going home

Pierre Castéran