### 1 ≠ 0

Learning Coq is usually an enlightening experience. I know it first-hand, it can also be a quite frustrating one, because it seems at first to involve remembering quite a lot of arbitrarily-named tactics, that one might not fully understand the effect of. `discriminate` is one of them: “if you’re faced with an obvious inequality, just apply `discriminate`” they say. If you look at the proof term, however, it is far from trivial and involves a “trick”, a kind of “lie” that Pierre has become a specialist of. There is an intermediate step in the comprehension, that we put together with Chantal: decomposing the proof generated by discriminate. Here is a very easy proof that 1 ≠ 0, which does not require to understand neither proof terms nor return clauses in pattern-matching. Pure beginner Coq.

It goes like this (in a very pedestrian style):

```Definition isZero x :=
match x with
| O => True
| S _ => False
end.

Lemma one_is_not_zero : ~ isZero 1.
simpl. intro H. destruct H.
Qed.

Lemma zero_is_zero : isZero 0.
simpl. exact I.
Qed.

(* By contradiction: suppose 1 = 0. Since 0 is null,
then so is 1. But by definition, 1 is not null, hence contradiction.  *)
Lemma zero_differs_from_one :  1 <> 0.
intro H.
apply one_is_not_zero.
rewrite H.
exact zero_is_zero.
Qed.
```

Play this proof step-by-step to discover the “lie”, that resides in the rewriting step.