Typo on natural number game

Stream: general

[YH]

In Inequality world, Level 3

Our hypothesis h is now ∃ (c : mynat), b = a + c (or a ≤ b if you elected not to do the definitional rewriting) so

cases h with c hc,

gives you the natural number c and the hypothesis hc : b = a + d.

Shouldn't the last one be hc : b = a + c?

[David Renshaw]

I agree! You could submit a pull request correcting it: https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world10/level3.lean#L34

[Kevin Buzzard]

Thanks! Will try to remember to fix :-)

[YH]

I agree! You could submit a pull request correcting it: https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world10/level3.lean#L34

Great. I just did.

Also https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world8/level1.lean#L20
this one should be succ_inj {a b : mynat} : (since it is used as succ_inj(hs) without specifying a and b) but I'm not sure if just changing it here will be enough to change it everywhere in the game so I didn't propose a change.