Stream: new members
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.
if I could get this, then I should be able to use
pow_succ and then
mul_zero and then
Eric Wieser (Feb 28 2021 at 08:26):
It's true by
thanks! Same idea as my previous tread then. is there a more direct way of getting there fwiw?
or alternatively, is there a way to enable tracing in the NNG? it would nice to see what lean is actually doing
Kevin Buzzard (Feb 28 2021 at 17:40):
Download the repo from GitHub and play with it in VS Code maybe. It's filed under ImperialCollegeLondon IIRC.
Lars Ericson (Feb 28 2021 at 19:22):
@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
Last updated: May 11 2021 at 00:31 UTC