If I define a custom set of natural numbers:

inductive mynat : Type
| zero : mynat
| succ : mynat → mynat

I can prove no successor is equal to 0 by defining a function using pattern matching:

def is_zero : mynat -> Prop
| mynat.zero := true
| (mynat.succ _) := false

theorem mynat_zero_ne_succ (a : mynat) : mynat.succ a ≠ mynat.zero :=
begin
    have r : is_zero (mynat.succ a) = is_zero (mynat.succ a),
    refl,
    conv at r {
        to_lhs,
        rw is_zero,
    },
    apply not.intro,
    intro h,
    rw h at r,
    rw is_zero at r,
    rw r,
    exact true.intro
end

Normally "no successor equals zero" is one of the Peano axioms. It has to be stated to get the natural numbers. But here it's apparently a theorem that you get as soon as you define the successor function.

I can see that what's going in here is something very fundamental in Lean about how inductive types or pattern matching work (and therefore how equality must work). The definition of the function, and the way it's used when rewriting, presupposes that zero is never of the form "succ _". I was wondering what that something actually is, and what it's called.