exercise 3.5.12 - how to do induction through an equivalence

Stream: Analysis I

[Rado Kirov]

I have x: Nat (our custom nats in Ch3), we don't have induction theorem in Ch3 AFAIKT, but obviously we can just use nat_equiv.symm to \N and do induction there. However when I write

induction' (nat_equiv.symm x) with x hx

I don't see a theorem (nat_equiv.symm x) = 0 in the first branch?

[Aaron Liu]

induction' h : nat_equiv.symm x with x hx (not tested)

[Rado Kirov]

That works indeed!

[Dan Abramov]

I sent a PR to stub this out — IMO this is very difficult to guess.

https://github.com/teorth/analysis/pull/306