Example. Inequality as an inductive [isa-002M]

inductive myLE :: "nat ⇒ nat ⇒ bool" where base: "myLE 0 n" | step: "myLE m n ⟹ myLE (Suc m) (n+1)"

Proving that this implies the normal inequality relation requires the use of variable generalising:

lemma "myLE m n ⟹ m ≤ n" apply (induct m arbitrary: n) apply simp apply (erule myLE.cases; simp) done