Proving elementary-algebra identities: now or later?

Stream: mathlib4

[Martin Dvořák]

Do you think that, if I postpone writing the chapter about proving elementary-algebra identities, advancement in Mathlib4 will allow me to write it much better in, let's say, 6 months from now?

[Martin Dvořák]

I am writing a study material about Lean 4. I got to a section about elementary-algebra identities and I realized that proving them is more difficult than I expected.

I can write the section now, of course, but I am wondering:
Will it get easier if I skip this section for now and write it later?

[Martin Dvořák]

Do you think that, if I write the section now, I will be motivated to rewrite it at the end of 2023 in order to show easier ways how to prove elementary-algebra identities?

[Martin Dvořák]

Basically I am asking you, who develop Mathlib4, for a guess whether you think that current ways of proving stuff like x > 0 → x + 1/x ≥ 2 will get obsolete soon.

[Martin Dvořák]

I am not asking about the specific theorem written above. I split it from the thread on fractional cancellation because I want to ask a soft question for the sake of planning my work.