Here is the extract from Gert Smolka’s book on computational type theory.

Isn’t it the case that within the third pattern, we apply negation to the variables obtained by discriminating both arguments and not the first one exclusively?

Here is my implementation of a function in Coq that returns true if and only if the first natural argument is less than the second. I use a recursive call applied to the variables obtained by discriminating both arguments within the definition, don’t I?

Fixpoint less_than (n m : nat) :=
  match n with
  | 0 =>
    match m with
    | 0 => false
    | S y => true
    end
  | S x =>
    match m with
    | 0 => false
    | S y => less_than x y
    end
  end.