Proving a pair isn't in a relation?

Question

I'm doing a homework problem and I'm not sure how to approach it. Basically I have to prove that two numbers share a relationship of being successors, and it was easy to prove that (2, 3) has this relationship. But how can I prove that (2, 4) does not? Here's my code so far.

inductive succ_rel : Nat → Nat → Prop
    | pair (a : Nat) : succ_rel a (Nat.succ a)

open succ_relation

example : succ_rel 2 3 := pair 2

--Not sure how to prove (2, 4) does not belong here

Answer 1

Use nomatch to prove that ¬succ_rel 2 4:

inductive succ_rel : Nat → Nat → Prop
  | pair (a : Nat) : succ_rel a (Nat.succ a)

example :  succ_rel 2 3 := succ_rel.pair 2
example : ¬succ_rel 2 4 := fun h ↦ nomatch h

You can also define the binary relation of one natural number being the successor of another as follows:

def Nat.isSuccOf (n m : Nat) : Prop := n = m.succ

example :  Nat.isSuccOf 3 2 := rfl
example : ¬Nat.isSuccOf 4 2 := fun h ↦ nomatch h
example : ¬Nat.isSuccOf 4 2 := by simp [Nat.isSuccOf]