bit0? how do I get succ(succ(0)) from 2?

Stream: new members

[eax]

I'm trying to prove ⊢ a ^ 2 = a ^ 2 + 0 ^ 2 (actually, part of (a + b) ^ (2 : mynat) = a ^ (2 : mynat) + b ^ (2 : mynat) + 2 * a * b := but ignore that for the moment) and think I need the fact that 2 = succ(succ(0)) but can't seem to get lean to output this. if I try one_eq_succ_zero I get a bit0 which I'm not sure how to deal with yet.

[eax]

if I could get this, then I should be able to use pow_succ and then mul_zero and then refl

[Eric Wieser]

It's true by rfl

[eax]

thanks! Same idea as my previous tread then. is there a more direct way of getting there fwiw?

[eax]

or alternatively, is there a way to enable tracing in the NNG? it would nice to see what lean is actually doing

[Kevin Buzzard]

Download the repo from GitHub and play with it in VS Code maybe. It's filed under ImperialCollegeLondon IIRC.

[Lars Ericson]

@eax there is a little more detail on bit1 in this thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/if.20a.20.3C.20b.20then.20a.5E3.20.3C.20b.5E3/near/224516939