Add bijective sticks and stones

[metakunt]

A truly horrendous proof...

[avekens]

A truly horrendous proof...

Would it be possible to extract some lemmas from the proofs to shorten them?

[metakunt]

It already is shortened by extracting the mapping proof of F and G first.
Most of the proof actually benefits from the shared context in previous statements, so I'm not quite sure if that would help that much.

On a different note, maybe there exists some helper theorem which application could "carry" context, yet I think the most helpful thing would actually be to just use deduction form theorems coupled with good autocomplete, which is sadly out of scope of this PR.

All in all I think a typescript for metamath would kinda be nice, i.e. a language which transpiles "typemath" (basically semantically knowledgable metamath with tactics) to metamath which had some basic tactics like SAT solving and simple tactics like conv and rw. But sadly there is no consensus in moving to that direction. Even simpler things like libraries and minimal (stable) API's are out of reach.

I've already tried to write a transpiler that certain natural number operations automatically and generates a valid metamath proof. It was actually pretty fun to do but ultimately pointless.