natural number game solution

Stream: general

[Joseph O]

For level 6 of Addition World, I came up with

rw add_assoc,
rw add_assoc,
rw add_comm c b,
refl,

and it works, but in the solutions, it had

rw add_assoc,
rw add_comm b c,
rw ←add_assoc,
refl,

is there anything different or better about the latter rather than the first?

[Joseph O]

It seems to be the same as mine, but just switching around the order. Is the latter solution more readable though?

[Eric Rodriguez]

no, they're both reasonable!

[Joseph O]

Which would you prefer?

[Arthur Paulino]

You should be able to say rw [add_assoc, add_assoc, add_comm c b], refl,

[Arthur Paulino]

(just to explore the syntax)

[Joseph O]

Arthur Paulino said:

You should be able to say rw [add_assoc, add_assoc, add_comm c b], refl,

they didn't show us that in the nat number game yet