NNG and change of induction basis

Stream: new members

[Kwame Porter Robinson]

I'm working on a natural numbers game level (World 9, Level 4), solved it, and am now exploring other proofs to that level. I know Lean has le_induction that starts from a different base case (e.g. n=1) but in NNG we have induction. Is there a way to change the basis of induction?

I attempted to do this with,

have a := 1 <= a, -- "error: failed to synthesize type class instance for for a b c : mynat,"
induction a with k h1,

In Lean 4
theorem mul_left_cancel2 (a b c : nat) (ha : a ≠ 0) : a * b = a * c → b = c := begin have a : 1 <= a,
gives

2 goals
abc: ℕ
ha: a ≠ 0
⊢ 1 ≤ a

abc: ℕ
ha: a ≠ 0
a: 1 ≤ a
⊢ a * b = a * c → b = c

and I can continue to solve the level with a different proof.

[Kyle Miller]

One way is to do cases a first, and for the second goal you do induction a like usual.