Definition of the predecessor function using small inversion

Pred.v

Inductive Nat := O : Nat | S : Nat -> Nat.
Inductive isSuc : Nat -> Prop := Indeed : forall (n : Nat), isSuc (S n).
Definition diag : Nat -> Prop :=
  fun n =>
  match n with
    | O   => False
    | S _ => True
  end.
Definition invert : isSuc O -> False :=
 fun isSuc0 => isSuc_ind diag (fun _ => I) O isSuc0.
Definition pred : forall n, isSuc n -> Nat :=
  fun n =>
  match n as n return isSuc n -> Nat with
    | O   => fun p0 => False_rect Nat (invert p0)
    | S m => fun _  => m
  end.